Tag Archives: Gaussian elimination

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.