All posts by msoos

Parallelisation

SAT

I have lately been reading the book Using OpenMP and thinking about how CryptoMiniSat could be parallelised. Apparently, there are multiple ways to achieve it. I haven’t yet had time to read through all previous approaches, but it seems there are at least two main ways to distribute the solving: through guiding paths and using the idea of ManySat.

The first approach, guiding paths, decomposes the problem into multiple sub-problems, setting some variables to true or false. The problems are then solved completely independently with a master coordinating the effort. I don’t like this approach for two reasons. Firstly, for cryptographic problems, the decomposition can be made very well since the problem in its most abstract form (i.e. key, plaintext, ciphertext) is known, and so a very good guiding path can be calculated. However, even with this very good guiding path, the expected total time to solve is far more than if the problem was given to one solver instance. In other words, if we decompose the problem into 4 sub-problems, and each sub-problem takes on average T time to solve, then the total average time is 4T, but if we gave the problem to one solver, it would have found the solution on average in e.g. 2T time. In other words, the gain is not as much as one would hope. I would guess that this ratio (2T/4T = 1/2 in this case) is even worse when the problem’s abstract form is totally unknown (which is most of the time), and the solver has to guess a guiding path.

The second approach, that of ManySat is to start the same solver with the same problem multiple times, but use different restart heuristics to solve the problem. Since modern DPLL-based SAT solvers use randomised algorithms, this helps to reduce the expected time to solve an instance. Also, the solvers share short clauses with one another to work in a more collaborative manner. However, I believe that given the distribution of the solving time of a problem with a given solver, even if more instances of it are launched (each with a random seed and different restart strategy), the minimum solving time of all launched solvers will not be as small as one would hope. It is extremely rare that a difficult instance can be solved in under e.g. 1 minute if the average time to solve it is 1000 minutes. So, if we were to launch 1000 solver instances, probably none would finish before 2-300 minutes. Of course I am not counting the effect of shared learnt clauses here, but I am not very convinced about them. Apparently, activity-based learnt clause sharing (instead of size-based) is more effective than size-based (see this), and ManySat shares them according to the size.

So, if all else fails, what is there left to do? Well, I bought the OpenMP book to find out. I wish to implement the idea of distributing clauses to different threads, thus distributing the BCP (Boolean Constraint Propagation) load. However, multi-threading can only go so far, so MPI will eventually need to be used, along with multiple instances of the solver on the same physical CPU, the way ManySAT is doing it — though I will try to implement some form of clause-sharing. The good thing is, that implementing MPI will also bring the possibility of running a problem instance on a huge cluster, something I am really looking forward to.

EDITED TO ADD (16/07/2010): I just realised that MiraXT does quite a number of things that I wish to implement into CryptoMiniSat.

Social coding

SAT,

I saw a talk by Ed Catmull on the problems Pixar had in their early days. The talk is very interesting, and I recommend it. What caught me, is that at Pixar they had a “brain trust”, a certain group of people who could express their new ideas to one another without fear of backlash. This is actually very difficult to achieve, since early implementations of ideas are always “childish”, lack maturity, and are therefore not considered good enough to be shared with others. However, if you don’t share the idea with the others early, then you will get feedback too late, when you have already invested a lot of time into it. Criticism at this late stage hurts more and what is worse, it might make you so uncomfortable, that you might abandon the idea altogether.

The trick is to get a set of people to trust each other well enough to share not-yet mature ideas with one another in the early stage, so that criticism can help everyone get their ideas right from the start. Establishing this trust is very difficult. I started to understand what Ed Catmull was talking about while working with the STP team. The earlier I seemed to share my ideas, the better they got. For instance, CryptoMiniSat was originally never meant to be used as a library. However, once they (mostly Vijay Ganesh) helped me debug the code, it was much easier to get things “right”. I also met Laurent Simon last year for half a day, and he gave me the idea of using Grid’5000 to test the performance of CryptoMiniSat. Without these early steering ideas, I would have never been able to get CryptoMiniSat to where it is today.

Blocked clause elimination implies dependent variable removal

SAT,

While writing the description of CryptoMiniSat for the 2010 SAT Race, I have realised how powerful the blocked clause elimination (BCE) technique by Matti Jarvisalo and Armin Biere is. For xor clauses, which represent a simple XOR like

v1 + v2 + v3 = true

there is a technique called dependent variable removal by Heule and Maaren. This technique removes an xor clause if one of its variables appears only in one place: in that xor clause. The idea is that since that variable only appears there, the XOR can always be satisfied. For example, if variable v1 is dependent (i.e. it only appears in this XOR), and

v2 = true, v3 = true

then this xor-clause can simply be satisfied by giving v1 = true:

true + true + true = true

So, variable v1 can be removed from the problem along with the xor clause, and the value of variable v1 needs only to be calculated after the solving has finished.

The great thing about blocked clause elimination, is that it can achieve this automatically, without the use of xor-clauses! Let us convert our xor-clause into regular clauses:

v1 v2 v3 (1)
v1 -v2 -v3 (2)
-v1 v2 -v3 (3)
-v1 -v2 v3 (4)

Now, let us try to block these clauses on variable v1. Resolving (1) with (3) gives tautology since the result of the resolution,

v2 v3 v2 -v3

has both a literal and its negation (v3 and -v3) in it. The same is true for resolving (1) and (4), this time with v2 and -v2. The same happens to (2)&(3) and (2)&(4), too, eventually removing all clauses.

So, can blocked clause elimination replace dependent variable removal? I am not sure. Dependent variable removal can be used in conjunction with other methods that treat xor caluses, that can lead to potentially very long XOR chains. These long XOR chains are not well handled through regular clauses, and so they are not created by solvers that don’t handle xor clauses natively — creating them is avoided through heuristic cut-offs. Thus, dependent variable removal can potentially remove more of these XOR-s than blocked clause elimination. But blocked clause elimination can remove clauses that dependent variable elimination cannot. So, I believe there is point in using both.

CryptoMiniSat v2 finally released

SAT,

CryptoMiniSat version 2.4.0 is finally here. I decided to use the INRIA Gforge system to coordinate bug-hunting, release management and the forums. However, the source code revision management is coordinated through Gitorious. There, you can find all revisions that have been made to CryptoMiniSat since its original SVN revision control was fixed to use trunk and branches. I believe at least a 1000 revisions are up, so you can see how the source evolved. The source now should be pretty stable, but I am looking forward to all bug reports and suggestons.

Gaussian elimination is currently disabled. It is present in the code, however, and can be enabled. The reason for disabling it is that I haven’t used it for quite some while. This means it needs testing to be stable, and some very minor tuning needs to be carried out to make work with the much updated internal state of CryptoMiniSat.

I hope this release is just a starting point for a number of upcoming releases that will be made in a much more transparent manner than they have been done until now. I am looking forward to feature requests, bug report and merge requests both in the Gforge and the Gitorious intefaces. Good SAT solving!

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…