Tag Archives: SAT Race

CryptoMiniSat in SAT Competition’11

SAT, ,

I have submitted three versions of CryptoMiniSat to the 2011 SAT Competition, all available here. The releases are commonly called “Strange Night”, after the music track of the same name. Inside the archive you will find 5 binaries and a PDF description. The five binaries are made up of two single-threaded, two multi-threaded, and a unified single- and multi-threaded binary. This latter is called techdemo, as it is more of a technological demonstrator than anything else, and was developed in collaboration with George Katsirelos and Laurent Simon. All versions are collaborative, however, as they all have the hands of some people from the CryptoMiniSat development mailing list on them.

To be honest, I am not overly optimistic of these binaries, especially since I couldn’t get the 3.0 version of CryptoMiniSat ready for the competition, on which I have been working on the past two months. I have tried to backport some features to the 2.9.0 branch to make these releases, and so the resulting executables are pretty unstable. The techdemo version is a broken 3.0 release, as it is missing the signature feature of fully shared clauses between threads. Since I have finally obtained a 4-core CPU — with hyper-threading for 8 “independent” threads — I am all the more optimistic about a fully-shared scheme. The upcoming 3.0 release will be specifically made to work in multi-threaded environments, and will suffer if launched in single-threaded mode. This architectural decision was made because multi-threading nowadays no longer seems optional: it’s a must. On the CryptoMiniSat mailing list, some people are reporting performance on 64-core machines — optimising for single-threaded environment (and having multi-threading as an afterthought) in these times seems like a broken approach.

For those interested in the actual sourcecode of what has been submitted, everything is available from GIT, as usual:

  1. Strange Night1 – single-threaded
  2. Strange Night1 – multi-threaded
  3. Strange Night2 – single-threaded
  4. Strange Night2 – multi-threaded
  5. Tech Demo

Since these are pretty unstable, I wouldn’t use them in a production environment… happy bug-hunting ;)

Creating a SAT solver from scratch

SAT, ,

I have lately been having a small chat with Francois Grieu and it inspired me to think about how difficult it would be to create a new SAT solver from scratch. Let’s take it for granted that the person who embarks on such a difficult task understands the basics well, and wishes to create a (nowadays very popular) Conflict-Driven Clause-Learning (or simply, CDCL) type SAT solver. The main parts of  these solvers are:

  1. Clause parser&database to store the clauses
  2. Propagation engine using watch-lists to carry out Boolean Constraint Propagation (BCP)
  3. Conflict generation code, using the first-UIP scheme
  4. Learnt clause activity calculator&deleter
  5. Variable state database, storing activity and polarity
  6. Search restart manager
  7. Pre-processor is recommended — SatELite does the job reasonably well.

None of these are very difficult to do. However, by implementing these in a minimalistic fashion, one will only end up with a reasonably fast, but not a very fast solver. Enhancements, for example, storing binary clauses implicitly in the occurrence lists in the database bring small, but nevertheless important, benefits. Similarly, having specialised watch-lists to handle binary and tertiary clauses further speed up the solving. Conflict clause minimisation, on-the-fly subsumption, and on-the-fly self-subsuming resolution improve conflict generation. Polarity-calculation and -caching comes handy for variable polarities, and dynamic restarts are also useful. Learnt clause activities might need to support both MiniSat-style and Glucose-style activities.

The real challenge, however, comes with bullet number 7: a fast and complete pre- and in-processor is very complex to write. The pre-processing done by SatELite, i.e. self-subsuming resolution, variable elimination and subsumption are just the icing on the cake for a good pre- and in-processor. Doing these in the middle of the solving (i.e. in-processing), using learnt clauses, doing asymmetric branching, binary clause reasoning, variable replacement, blocked clause elimination, failed literal probing, tautology elimination, clause strenghtening with tautological binary clauses, clause cleaning, and a long list of others — that’s where the hard part lies.

With all of these challenges facing SAT solver implementers, is it reasonable to think that anyone can relatively easily participate in SAT Races and SAT Competitions? If one wishes to respond with yes to this question, then there are two paths ahead: either immense amounts of time need to be invested into writing such a solver, or an already written solver has to be taken as a base to build ideas upon.  I think the only reasonable choices for a base are: lingeling, MiniSat, PrecoSat and (I hope to think) CryptoMiniSat. None of these solvers are perfect of course, so one has to put up with all the inherent problems in these solvers.

In the past months, I have been writing many blog entries trying to detail the inner workings of SAT solvers — mostly to help others (and in the process, myself) struggling with SAT solvers. Maybe I should be spending more time trying to document the code of CryptoMiniSat, so that the barrier for entry to creating winning SAT solvers could be lowered.

Winning the SAT Race

Personal, SAT

The software I developed, CryptoMiniSat 2.5 won the SAT Race of 2010. It is a great honour to win such a difficult race, as there were 19 other solvers submitted from 9 different countries.

Thinking back and trying to answer the question why CryptoMiniSat won, I think there are no clear answers. Naturally, I put immense effort into it, but that is only one part of the picture. Other important factors include those who supported me: my fiancée, the PLANETE project of INRIA, and in particular Claude Castelluccia and my colleagues here in Paris, the LIP6 team and my professor here, Jean-Charles Faugere. As with all randomised algorithms, luck played a good part of winning, too.

In all of this, it is interesting to note that I never had a colleague who worked in or even near the field of SAT: both the PLANETE and the LIP6 team use SAT solvers only as a means to an end, not as an end in itself. In other words, I had to get this far mostly alone. To be honest, I think this is one of the reasons I had won, too: there probably is too much misunderstanding in SAT that everybody takes for granted. Since I never really talked with anyone about their understanding of the subject (I only read papers, which state facts), I had a white paper in front of me, which I could fill with my own intuitions, without being lead by those of others. Naturally, this means that I have probably stepped into a large number things that are widely understood to be wrong, but at the end, it seems that I must have also made some good steps, too.

As for the bad steps I have made (and of which I am aware of), I had copied the subsumption algorithm from SatElite, which the authors of MiniSat told me was a bad move, since its self-subsuming resolution is slow. I had in fact observed this, but I thought it was a fact of life. Alas, it isn’t. Other errors I have made include a non-portable pointer-shortening which shortens pointers to 32 bits when using 64-bit architectures (Armin Biere’s lingeling does this right), and a wrong clause-prefetching code that Norbert Manthey put me right about. I have also conceptually misunderstood the possible impact of variable elimination on the difficulty of resolving an instance, a grave mistake that Niklas Sörensson put me right about.

As for the good steps, I think I have made a couple of them. Firstly, I have put the 2009 SAT paper we wrote with my colleagues to its natural conclusion: including XOR clauses and partial XOR reasoning into the innermost parts of the solver. Secondly, I have used the community to its fullest potential: CryptoMiniSat was used by the constraint solver STP far before the SAT Race began, and it was distributed to a number of highly skilled individuals who made use of it and gave feedback. Sometimes I got very negative feedbacks (these were the most valuable), which highlighted where and why the solver was failing. Thirdly, I have tried to take advantage of the academic environment I work in: I have tried to read the relevant papers, used the clusters provided by the French universities to carry out experiments, and generally took my time (rarely an option in industry) to get things right instead of rushing out a solver.

The Obvious Child

SAT, ,

The new CryptoMiniSat 2.5.1, codenamed “The Obvious Child” has been released. It’s very close to the system that has been sent into the SAT Race’10. This version of CryptoMS is much better than any versions before: I finally corrected a lot of bugs that went into the 2.4.x series, and added new features to treat binary clauses.

The release name is the song title by Paul Simon. I am a fan of the 60’s for many reasons. It was the time when Laing wrote his first books, empathy was first scientifically demonstrated for animals, the days of I have a dream, the landing on the moon, and the take-off of Simon&Garfunkel.; Some interesting times, shall we say.

I probably will be working less on CryptoMiniSat from now on, instead concentrating on other things that I must do, such as publishing research papers on subjects that interest the scientific community. I will also be trying to play out in my mind how CryptoMiniSat will fare in the SAT Race. Of course I am hoping for the best, but I worked on the program for a mere 8 months, alone. Comparing this to some experts working on their solvers for multiple years in groups of 2-3, I really have no chance of winning. However, I am optimistic, as always: maybe I will get some good position in the rankings :)

On PrecoSat

SAT,

Lately, I have been having a poll of who will win the SAT Race’10. Apparently, 5 people voted until now, me included. I voted PrecoSat. Not because I didn’t want to vote CryptoMiniSat, but because I honestly believe it really will win. The reason is awfully simple: Armin Biere, the (main) author of PrecoSat has had far more experience and time than me to perfect his solver. This is normal, though I only hope he might notice the amount of effort that was put into CryptoMiniSat.

CryptoMiniSat now contains ~10’000 lines of code, compared to the original so-called ‘core’ MiniSat it has been developed from, which contained ~1’000. A ten-fold increase in code, which represents more than 1300 commits in the main tree (and about 1.5 years of my life). This effort has not been carried out alone. Though I haven’t much talked about people that helped me on the way, CryptoMiniSat has been tested and patches have been committed by a number of people, putting a lot of their time and effort into making a working SAT solver. They all worked just for the fun of being part of the project.

The collaborative nature of the CryptoMiniSat project is partially the reason why, I hope, it might succeed in the end in becoming a viable alternative to PrecoSat. End of next week, I will post the whole revision history of CryptoMiniSat to Gitorious, so everyone can see how certain options evolved over time — my commit messages are usually (overly) long ;) Then, bugzilla, mailing lists, forums and the rest will hopefully garner some steam, and we can start rolling. The road is wide ahead…