CryptoMiniSat 5.0.0 released

CryptoMiniSat 5.0.0, after winning the incremental track at SAT Competition 2016 and getting 3rd place at the parallel track, has been released. The new solver contains a number of important additions. The most important are that the solver can now be used as a preprocessor and Gauss-Jordan Elimination is back.

Why CryptoMiniSat 3.3 doesn’t have XORs

I’ve had a number of inquiries about why CryptoMiniSat 3.3 doesn’t have native XOR clause support. Let me explain what I think the benefits and the drawbacks are of having native XOR support and why I made the choice of removing them.

Benefits

The most trivial benefit is that users don’t have to translate XORs into plain CNF. Although transforming is rather easy, some prefer not to go through the hassle. The principle is to cut the XOR into smaller XORs by introducing new variables and then representing the cut-down XORs by banning all the wrong combinations. For example the the XOR $x+y+z+w=0$ is cut into two XORs $x+y+r=0$, $z+w+r=0$ and then $x+y+r=0$ is represented as $x \vee y \vee r, x \vee \neg y \vee \neg r, \ldots$.

A more substantial benefit is that propagation and conflict generation can be done natively. This is quite advantageous as it means that far less clauses and variables need to be visited while propagating and generating the UIP conflict. Less variables and clauses visited means less cache-misses and due to the more compact representation, less memory overhead and thus even better cache usage. (For the aficionados: an interesting side-effect of XORs is that blocked literals cannot be used for XOR clauses).

The biggest benefit of having native XORs is that Gaussian elimination can be carried out at every level of the search tree, not just at top-level. Although most people I have talked with still think that CryptoMiniSat 2 only performs Gaussian elimination only at top-level, this is not the case. Performing Gauss at top-level is a two-day hack. Performing it at every level took me about half a year to implement (and about 5K lines of code). It requires leaving traces of past computations and computing reasons for propagations and conflicts indicated by the Gaussian elimination algorithm. According to my highly unofficial count, exactly 2 people use Gaussian elimination at deeper than top-level, Vegard Nossum and Kuldeep S Meel. Out of these two users, only the latter have indicated speedups. It speeds up crypto problems, but not many others, so it’s completely disabled by default.

Drawbacks

The main drawback of having native XOR clauses along normal CNF clauses is the loss of simplicity and universality. Let me explain in detail.

Loss of simplicity. Once a variable present in both a normal and an XOR clause, it cannot be eliminated in a simple way. I don’t even want to try to express the clauses that would result from doing varelim in such cases — it’s probably horribly convoluted. All algorithms in the code now need to check for XORs. On-the-fly clause strengthening cannot strengthen an XOR with a normal clause, of course. Clause cleaning has to take into account that when a 3-long XOR is shortened to a 2-long one, it indicates a new equivalent literal and that may lead to immediate UNSAT. I could go on, but the list is long.

Another problem is that XORs make the state more complex. Until now there were only clauses of the form $a \vee \neg b \ldots$, sometimes specially stored such as binary clauses. The state of the solver goes through many transformations — think of them as llvm passes — while it is in-processed and solved. The more complex the state, the larger and the more complex the code. While a simple clause-cleaning algorithm can be expressed in about 20 lines of code without implicit binary&tertiary clauses, the same algo blows up to about 100 lines of code with those optimizations. Once you add XOR clauses, it jumps to around double that. We just made our code 10x larger. Imagine adding native support for, e.g. at-most-n.

Loss of universality. If a variable is only XOR clauses, it can now be eliminated at the XOR level. A pure variable at the XOR level indicates an XOR clause that can be removed and later always satisfied. XOR subsumption is when an XOR subsumes the other: the larger can be removed and their XOR added in. All of these are implemented in CMS 2. Probably there are many others out there, though. We could try to implement them all, but this is a whole new universe that may open up the gates of hell. Worst of all, most of these techniques on XORs are probably already simulated by in-processing techniques at the CNF level. Pure XOR variables are simulated by blocked clause elimination. XOR-based variable elimination doesn’t make practical sense at the CNF level, but it could be simulated by normal variable elimination if ignoring heuristics. I could go on.

What CryptoMiniSat 3.3 does

The compromise I came up with for CryptoMiniSat 3.0 is that I regularly search for XOR clauses at the top-level, perform top-level Gaussian elimination, and add the resulting new information to the CNF. Binary and unitary XOR clauses are the simplest to add back.

In the SAT’11 application benchmark set, out of 300 problems, 256 problems contain XOR clauses. the number of XOR clauses found, when they are found, is on average 2905 with an average size of 4.2 literals. Using Gaussian elimination, counting only when something was extracted, the average number of literal equivalences (binary XORs) extracted is 130, while the number of unitary clauses extracted is 0.15.

Here is a typical example output:

Here, about 104K XOR clauses were found (using a sophisticated algorithm) within 2.11s, all of size 3. These XOR clauses were subjected to disconnected component analysis (within the XOR sphere) and they were found to belong to 2185 components. It is important to cut XORs into groups, because Gaussian elimination is an $O(n^{\approx 2.5})$ algorithm and if we can reduce the n by having more than one matrix, the speed is significantly increased. Next, these 2185 matrices were Gauss-eliminated and were found to contain 1275 binary XOR clauses, which were quickly marked as equivalent literals.

To perform Gaussian elimination at top-level, CryptoMiniSat uses the excellent m4ri library, maintained by my old college and friend Martin Albrecht. It’s a lightweight yet extremely fast Gaussian elimination system using all sorts of nifty tricks to do its job. Unfortunately, for large matrices it can still take a long while as the algorithm itself is not cheap, so I have a cut-off for matrices that are too large.

What a future CryptoMiniSat 3.x could do

Once we have extracted the XORs, we could just as well keep them around during search and perform Gaussian elimination at levels below the top-level. This would bring us close to the old system in terms of real performance — native propagation (which would be unavailable) can only give a 1.5x-2x speedup, but Gaussian elimination at every level can give much more. I would need to clean up a lot of code and then, maybe, this would work. Maybe I’ll do this one day. Though, after spending weeks doing it, probably people will still believe it only does top-level. At least right now, it’s the case.

Conclusions

Implementing a new theory such as XOR deep into the guts of a SAT solver is neither easy nor does it provide a clear advantage in most situations. Those who push for these native theories have either not tried implementing them into a complicated solver such as lingeling/SatELite/CryptoMiniSat/clasp or have already bit the bullet such as the clasp group and I did, and it is probably limiting them in extending the system with new techniques. The resulting larger internal state leads to edge cases, exceptions, and much-much more code.

Gaussian elimination is released

The new CryptoMiniSat, version 2.4.2 now has on-the-fly Gaussian elimination compiled in by default. You can simply use it by issuing e.g.

`./cryptominisat --gaussuntil=100 trivium-cipher.cnf`

and enjoy outputs such as:
`c gauss unit truths : 0c gauss called : 31323c gauss conflicts : 5893 (18.81 %)c gauss propagations : 7823 (24.98 %)c gauss useful : 43.79 %c conflicts : 34186 (4073.39 / sec)c decisions : 39715 (6.86 % random)`
Which basically tells that gaussian elimination was called 31 thousand times out of 39 thousand, and so it was essentially running almost all the time. Out of the 31’323 times it was called, 44% of the cases it found either a conflict or a propagation. This is a very good result, and is typical of the Trivium cipher. Trivium can be speeded up by up to 2x with Gaussian elimination. I will put up lots of CNFs, so you will be able to play around with them and (optionally) verify these results.

The magic parameter “–gaussuntil=100” tells the program to execute Gaussian elimination until decision level 100, and no deeper. I haven’t implemented and automation into finding the best depth, and so I use this (very) crude fixed number 100. Probably better results could be achieved with a fine tuning of the depth cut-off, but I don’t have the time for the moment to play around with it. However, if you are interested, you will be able to try out different depths, different ciphers, etc. I will shortly be releasing a tool called “Grain of Salt” to generate CNFs for any shift-register based stream cipher, so you can test them against CryptoMiniSat or any other SAT solver.

I hope you will enjoy using on-the-fly Gaussian elimination in CryptoMiniSat 2.4.2!

CryptoMiniSat v2 finally released

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!

Why CryptoMiniSat can’t use MATLAB to do Gaussian elimination

Some people, who may not have thought through the problem of implementing Gaussian elimination into SAT solvers, seem to think that it’s just a matter of pulling a matlab function into a solver, and the job is done. Let met explain why I think this is not the case.

Firstly, we don’t wish to execute Gaussian elimination simply before the solving, instead, we wish to execute it during the solving. This means the matrix’s columns need to be changed often, since as we move down the search tree, some variables will be fixed, thus the columns need to be cleared, and the augmented column needs to be updated. But how would a matlab function know which column was changed? These functions are made to work on any given matrix, churn through it, and finish with a result. However, in many cases, the change (=delta) between two matrixes is minimal (i.e. 3rd column from right was changed). In this case, the matlab routine will nevertheless start updating the matrix from the leftmost column, essentially taking far more time than an algorithm that knows that the delta was small.

Secondly, let’s assume that a value like “x1=true” has been found by the matlab function. Since we don’t know where this information came from, there is only one way of adding it: put it into the propagation queue. This, however, would be a grave mistake. By not giving the solver a hint where this propagation came from, the solver cannot use this information during conflict generation, and we will loose most of the benefits. In case a conflict is found by our matlab function, the problem is even worse. What caused the conflict? We simply don’t know. We can send the solver back one decision level, and hope for the best, but non-historical backjumping is one of the main reason SAT solvers perform so well. On the other hand, if we keep another matrix, not assigned with the current assignements but updated with all row-xor and row-swap operations (as in CryptoMiniSat2), then we will have all these informations at our disposal, and the integration of Gaussian elimination into the SAT solving process will be correct.

These two reasons should be sufficient to see that matlab, or really any mathematical package that implements Gaussian elimination is not useful for CryptoMiniSat. Yes, some of their “tricks” could be used, and I think are already being used.

PS: As a side-note, many have told me that the matrixes are sparse, and so I should use a sparse matrix data structure. Although the matrixes are indeed sparse, they are also miniscule. On very small matrixes (<200-300 columns) there is simply no point in doing sparse matrix elimination. Not to mention, that since two different matrixes need to be stored and handled, it is impossible to find a pivot that is optimal for both, thus the density of at least one of the matrixes must evolve faster than optimal, leading to an early switch to a dense matrix representation.