Tag Archives: Parallel SAT Solving

MapleCOMSPS taking the cake

I’ve been reading through the source code of the 2016 SAT Competition winner, MapleCOMSPS_DRUP, and this piece of beauty hit me:

Continue reading

CryptoMiniSat: 8000 commits later

The GitHub repository for CryptoMiniSat just hit 8000 commits. To celebrate this rather weird and crazy fact, let me put together a bit of a history.

The Beginnings

CryptoMiniSat began as a way of trying to prove that a probabilistic cryptographic scheme was not possible to break using SAT solvers. This was the year 2009, and I was working in Grenoble at INRIA. It was a fun time and I was working really hard to prove what I wanted to prove, to the point that I created a probabilistic SAT solver where one could add probability weights to clauses. The propagations and conflict engine would only work if the conflict or propagation was supported by multiple clauses. Thus began a long range of my unpublished work in SAT. This SAT solver, curiously, still works and solves problems quite well. It’s a lot of fun, actually — just add some random clause into the database that bans the only correct solution and the solver will find the correct solution. A bit of a hackery, but hey, it works. Also, it’s so much faster than doing that solving with the “right” systems, it’s not even worth comparing.
Continue reading

Multi-threading

Just a short note: this Easter holiday I got a bit bored and did a mini-threading system for CryptoMiniSatv4. It will now be able to compete in the multi-threading track after quite a number of years of absence. Last time I did this, CryptoMiniSat won the UNSAT multi-threaded track, which was a bit funny because all I shared were unitary and binary clauses. For the simplicity and the fun, I’m doing the same this time around. Let’s hope all the super-complicated and extra-theoretical stuff will get won over.

Non-blocking datastructs

Some authors implement a non-blocking data-sharing construct to gain more performance out of the system. I think/hope that what is shared is more important than how. I use one global lock for the shared unit and one for the shared binary clauses. Since there won’t be more than 8 threads under normal circumstances and I have to lock about once per 10sec per thread for about 0.01s, there won’t be any contention. Under these circumstances, simplicity wins over the complexity of using non-locking datastructures. Also, these fancy datastructs probably don’t have an implementation that is C++11 (i.e. portable) and is already implemented in gcc 4.7.1 (which doesn’t support a number of the threading constructs), the compiler used in the competition.

Library usage

This time around I didn’t mess it up: multi-threading can be used from the library interface. The system completely hides the fact that multiple threads are competing in the background to solve the problem. The threads are cleanly and safely stopped and then re-started when the user asks for another solve() operation, optionally with assumptions. In other words, the user doesn’t see and doesn’t have to bother with the complexity of threads. All of that is abstracted away behind a neat and clean API. This means that e.g. the different threads can have radically different variable numbers. They could have renumbered the variables differently, added new and different BVA variables, etc. All of this is hidden away and the user is presented with and always communicates using his/her own variable numbers.

Final notes

This simple multi-threading system means that I can now port my old MPI code to use the new CryptoMiniSat. Maybe, once again, CryptoMiniSat will run on a cluster. Fun times ahead!

CryptoMiniSat won two gold medals at SAT Comp’11

(Note: the judges made a small mistake, and CryptoMiniSat only won 1 gold and 1 silver medal. Details below.)

CryptoMiniSat‘s SAT Competition’11 version, “Strange Night” won two gold medals at the competition: one shared with lingeling at the parallel SAT+UNSAT Applications track, and one at the parallel UNSAT Applications track. This is a great result, and I would like to thank everyone who helped me and the solver achieve this result: my fiancée, my current employer, Security Research Labs and Karsten Nohl in particular, who started the whole CryptoMiniSat saga, my former employer, INRIA Rhone-Alpes and in particular Claude Castelluccia, and finally, all the kind people at the development mailing list. Without the help of all these people, CryptoMiniSat would probably never exist in the first place, much less win such distinguished awards.

The competition was very though this year, and so it is particularly good that we have managed to win two gold medals. The most gold medals were won by the portifolio solver ppfolio, winning 5 gold medals — all other solvers won at most 2 gold medals. CryptoMiniSat did very well in the parallel applications track, basically winning all gold medals that ppfolio didn’t win — and ppfolio was using an older version of CryptoMiniSat as one of its internal engines, essentially making CryptoMiniSat compete with itself (and other strong solvers such as lingeling and clasp). Unfortunately, CryptoMiniSat didn’t win any awards at the sequential applications track, as most awards there were won by very new solvers such as Glucose ver 2 and GlueMiniSat. The source code and PDF description of these solvers are not yet available, but they will be shortly at the SAT Competition website.

Overall, I think CryptoMiniSat did very well, considering that I was not very optimistic given the fact that I didn’t manage to finish the new generation (3.x) of the solver, and had to submit a variant of the very old CryptoMiniSat 2.7.0. Furthermore, in the past year I have been concentrating on ideas external to the clause learning of SAT solvers, and it seems that the best way to speed up SAT solvers is to attack the core of the solver: the learning engine. So, this year will be about cleaning up all the external ideas and implementing new ones into the core of the solver.

Once again, thanks to everyone who helped CryptoMiniSat get such high rankings, and I am looking forward to the next year for a similarly good competition!

Edited to add (29/06):  The judges just informed me that they made a mistake, and the originally presented results were erroneous. CryptoMiniSat won 1 gold and 1 siver, as lingeling was faster by about 7% in speed in the parallel SAT+UNSAT track. Congratulations to Armin Biere for winning this track!

Dreaming up a parallel SAT architecture

When someone looks at the speed of solving when using parallel SAT solvers, it is easy to see that scaling doesn’t really work — especially for the hard UNSAT problems. In the past months I have been struggling to think of an architecture that will enable me to write a SAT solver that solves this problem. Let me share with you where I got. It will be more of a brainstorming than a descriptive blog post, but maybe it will help you avoid pitfalls, or maybe just to get a better picture of parallel SAT solving.

The constraints:

  • Clauses must be shared… all the time. Not “when it’s good enough” as per ManySat — that architecture doesn’t work well for UNSAT problems. The performance of a fully shared scheme should be able to overtake a ManySat-like architecture with ease. Only sharing low-glue or high-activity clauses does not work. This is easy to test: write a single-threaded SAT solver with high-glue learnt clause detaching on backtracking. It will work decidedly worse, even though you would clean those clauses anyway when doing clause cleaning. The reason? I don’t know… probably we need those clauses in our current local (=var activities similar) search.
  • Clauses need to have glues and activities. Glues could be dynamically updated, but the gain is not that much and the burden is a bit too much — so make that static. Activities (which are inherently dynamic) are important though (see CryptoMiniSat), and they must be lock-free as they would need to be updated frequently.
  • Memory is scarce when implication caching is used. Implication cache must be shared and updated across the parallel solvers. This not only lowers memory usage, but is an important way to share information other than clauses.
  • Parallel solvers must be lean otherwise the burden of programming a correct solver would be far too much
  • Simplifications must be carried out regularly, which needs the coordinated stopping / interruption of all parallel solvers

My architectural solution:

  • Make a lean class that only handles: clause attachment, detachment and propagation. I will need to add on-the-fly hyper-binary resolution and on-the-fly useless binary clause removal as well, as those are tightly coupled to propagation
  • Make a class that handles search&conflict generation. This class has the lean class as parent. This generates conflict clauses and has its own variable & clause activities. The class checks for new conflict clauses form other solvers after every conflict it generates, and attaches those clauses when that doesn’t need trail-rewriting — though this latter could be made optional. This class does not store a list of clauses. The tricky part of this class is on-the-fly subsumption. We will handle that by not shortening the clause but instead adding a new one and detaching the old one. The thread-coordindating class will handle the propagation of this update to all other threads. Checks for interruption are done after every generated conflict.
  • A thread-coordinating class that handles clause storage, clause distribution, and simplification. This class stops all threads if UNSAT or SAT is found by one thread, and interrupts them if clause-cleaning needs to be carried out. This class also has the lean class as parent, since e.g. clause vivification or variable-replacement need propagation.

Data structures:

  • Fully shared clauses. No move-to-front strategy, instead literal-sorting is carried out once in a while (during simplification I would assume). This has already been implemented, and is only about 10% slower than non-shared clauses in single-threaded mode.
  • Interrupt handler. This is just a flag set by the coordinating solver. The subsolvers check this flag after every conflict generated, and either exit (if SAT/UNSAT is found) or just stop and mark each learnt clause locked (if cleaning the learnt clause database)
  • Implication cache. Needs read-write lock, as most of the time it will be read to do on-the-fly self-subsuming resolution with non-existent binary clauses. Can only have literals added, not removed. Removal and updating of literals is performed only during simplification. Updating (i.e. writing) is done by threads only when doing propagation at decision level 1.
  • Distribution of newly learnt clauses. A ‘lock-free’ (how I don’t like this — it’s misleading, it has locks) datastructure for each thread in the thread-coordinating class that allows the storage of a pre-fixed number of clauses, accessible & writeable without locks until the buffer is filled (at which point we lock & update pointers).

Dilemmas:

  • Maybe thread-management while searching (i.e. learnt clause cleaning and sharing) should be a different class from the one that performs simplification. The former would not need to have propagation at all. Separation of duties always leads to cleaner code.
  • Single-threaded solving is now only an afterthought, and it would be interesting to see how the solver performs in single-threaded mode. I hope it will be only slightly worse than if it didn’t have this architecture around it. It is interesting to note, though, that the structure of the solver will be much cleaner than huge-blob single-threaded solvers tend to be.
  • OpenMP will probably not suffice, as read-write locks are not available, and implication cache sharing is a very important part of the architecture. Fully locking that datastructure when using it would incur too much overhead — most (99.9%) of the time we will be reading it. This means the code might not be as portable as I wished it would be. I think the read-write lock is the only thing I am missing to implement all of this using OpenMP.

Notes:

  • This architecture lets the designer easily change the propagation mechanism. Just re-write the lean class. I have actually done that, and I can have both move-to-front (does not work with sharing) and static clause propagation strategies. People could write their own with ease.
  • Conflict generation&search class should have an object pointer passed to it that is an instance of a class that has a abstract search class as its parent. We could then change restart settings on-the-fly by passing different object pointers.
  • We could save state (i.e. stop&restart search) easily by interrupting all threads and saving the clause database (+learnt clause cleaning state). Simplifications should be fully stateless, so no state would need to be saved for those.

Okay, this is as far as I got. I have the lean class and the search&conflict generation class, the shared clause architecture, and the stateless simplifications ready, but the coordinating class is currently highly entangled with the conflict generation class, so those need to be separated. Further, I want to fix on-the-fly subsumption because it seems to be an easy way to improve the efficiency of conflict generation: if we can shorten a non-learnt clause at every 10th conflict, that is essentially a surely good conflict clause that will never be cleaned. The effect of not having to clear clauses is important when e.g. 6x more conflicts (for a 6-core CPU) are being generated per second than with a single-threaded solver.