Tag Archives: Parallel SAT Solving

CryptoMiniSat and Parallel SAT Solving

Development, Research, SAT

Since CryptoMiniSat has been getting quite a number of awards with parallel SAT solving, it’s about time I talk about how it does that.There is a ton of literature on parallel SAT solving, and I unfortunately I have barely had time to read any of them. The only research within the parallel SAT solving area that I think has truly weathered the test of time is Plingeling and Treengeling — and they are really interesting to play with. The rest most likely  has some merit too, but I am usually suspect as the results are often –unintentionally — skewed to show how well the new idea performs and in the end they rarely win too many awards, especially not in the long run (this is where Plingeling and Treengeling truly shine). I personally haven’t published what I do in this scene because I have always found it to be a bit too easy and to hence have little merit for publication — but maybe one day I will.

Note: by unintentionally skewed results I mean that as you change parameters, some will inevitably be better than others because of randomness in the SAT solving. This randomness is easy to mistake for positive results. It has happened to everyone, I’m sure, including myself.

Exploiting CryptoMiniSat-specific features

CryptoMiniSat has many different inprocessing systems and many parameters to turn them on/off or to tune them. It has over 60k lines of code which allows this kind of flexibility. This is unlike the Maple*/Glucose* set of solvers, all coming from MiniSat, which basically can do one thing, and one thing only, really well. That seriously helps in the single-threaded setup, but may be an issue when it comes to multi-threading. They have (almost) no inprocessing (there is now vivification in some Maple* solvers), and no complicated preprocessing techniques other than BVE, subsumption and self-subsuming resolution. So, there is little to turn on and off, and there are very few parameters — and the few parameters that are there are all hard-coded into the solver, making them difficult to change.

CryptoMiniSat in parallel mode

To run in parallel mode, CMS takes advantage of its potential heterogeneity by running N different threads, each with radically different parameter settings, and exchanging nothing but unit and binary clauses(!) with the most rudimentary locking system. No exchange of longer clauses, no lockless exchanges, no complicated multi-lock system. One lock for unit clauses, one for binary, even for 24 threads. Is this inefficient? Yes, but it seems good enough, and I haven’t really had too many people asking for parallel performance. To illustrate, here are the parameter sets of the different threads used and here is the sharing and locking system. It’seriously simple, I suggest you take a peek, especially at the parameter sets.

Note that the literature is full of papers explaining what kind of complicated methods can be used to exchange clauses using different heuristics, with pretty graphs, complicated reasoning, etc. I have to admit that it might be useful to do that, however, just running heterogeneous solvers in parallel and exchanging unit&binary clauses performs really well. In fact, it performs so well that I never, ever, in the entire development history of 7 years of CMS, ran even one full experiment to check parallel performance. I usually concentrate on single-threaded performance because checking parallel performance is really expensive.

Checking the performance of a 24 thread setup is about 15x more expensive than the single-threaded variant. I don’t really want to burn the resources for that, as I think it’s good enough as it is. It’s mostly beating solvers with horrendously complicated systems inside them with many research papers backing them up, etc. I think the current performance is proof enough that making things complicated is not the only way to go. Maybe one day I will implement some more sophisticated clause sharing, e.g. sharing clauses that are longer than binary and then I won’t be able to claim that I am doing something quite simple. I will think about it.

Conclusions

I am kinda proud of the parallel performance of CMS as it can showcase the heterogeneity of the system and the different capabilities of the solver. It’s basically doing a form of acrobatics where the solver can behave like a very agile SAT solver with one set of parameters or like a huge monolith with another set of parameters. Since there are many different parameters, there are many different dimensions, and hence there are many orthogonal parameter sets. It’s sometimes interesting to read through the different parameter settings and wonder why one set works so much better than the other on a particular type of benchmark. Maybe there could be some value in investigating that.

Non-reproducible results with MapleCOMSPS

SAT

I’ve been reading through the source code of the 2016 SAT Competition Main Track winner, MapleCOMSPS_DRUP, and I found that it has an important piece of code, regulating its behaviour that depends on timing:

static bool switch_mode = false;
static void SIGALRM_switch(int signum) { switch_mode = true; }

lbool Solver::solve_()
{
    signal(SIGALRM, SIGALRM_switch);
    alarm(2500);

Continue reading Non-reproducible results with MapleCOMSPS →

CryptoMiniSat: 8000 commits later

Personal, SAT, , ,

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 CryptoMiniSat: 8000 commits later →

Multi-threading

SAT

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

SAT, ,

(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!