Tag Archives: bug

On hyper-binary resolution

Research, SAT, ,

Hyper-binary resolution is actually quite straightforward, or at least appears to be. Let’s take the following example. The clauses in our database are the following:

-a V b
-a V c
-b V -c V g
-b V -c V d
-d V g

Let’s set a to true, and see what happens. Immediately, b and c get set to true through binary clauses. If we now propagate g through the clause -b V -c V g, we ought to do hyper-binary resolution straight away, and add the clause -a V g — some call this lazy hyper-binary resolution. Good, one more binary clause!

But then… So now we have nothing to propagate using only binary clauses, we have to propagate using a long clause, -b V -c V d. As good citizens, we also do (lazy) hyper-binary resolution, coming up with the clause -a V d. Good, one more binary clause! One slight glitch now… d propagates to g, using a binary clause. But this means that setting a can propagate to g without -a V g, the first hyper-binary clause we added! So the first hyper-binary clause we added is in fact useless, it needs to be removed. If we applied transitive reduction, it would remove the first hyper-binary clause -a V g automatically.

Let’s go a bit deeper here. How could we have avoided adding the first hyper-binary clause? The obvious answer is: we should have started with -b V -c V d instead of -b V -c V g. But how easy would have it been to know (i.e. calculate) that starting with that different long clause would have made our work easier? I am not sure it would have been easy to know. And of course the example above is very trivial. It could be made much-much more complicated: g could have been reached with any number of hyper-binary resolutions from d — so simple binary look-ahead would not have helped.

I am stuck here. Any ideas?

Implicit binary clauses

SAT, ,

I have lately been trying to get CryptoMiniSat to use implicit binary clauses. The idea is that since binary clauses are very trivial (just two literals), and they don’t really need to keep state (like clause activity), they don’t really need to be stored at a separate location. Instead, they can be stored directly in the watchlists. There are a number of advantages and disadvantages that come with this approach.

The main advantage is a notable reduction of memory usage and memory fragmentation. The first is obvious: since we don’t allocate space for binary clauses separately, the memory usage of the program should go down. This is especially true since SAT problems usually contain a huge number of binary clauses. The secondary benefit, that of reduced memory fragmentation is not really that much of an advantage if someone uses, e.g. the boost pool library.

The disadvantages are mainly twofold. Firstly, bugs are very difficult to find. Since there is not one central database of binary clauses (as before), it becomes difficult to check the consistency of the watchlists. However, if inconsistencies creep in, then the solution found by the SAT solver could be wrong. Worst of all, consistency is difficult to keep, as binary clauses often need to be worked on by e.g. subsumption, variable elimination, etc. The second biggest disadvatage is that if a new algorithm comes up that needs a database of binary clauses, this database would need to be re-built every time to run that algorithm, which can be very costly in terms of time.

All in all, it took me about 1 day to implement implicit binary clauses, and about 3 days to debug it. Surprisingly, it came with some very positive side-effects. Firstly, the debugging session took out some very long-standing bugs in CryptoMiniSat. Secondly, since binary clauses represent most clauses in typical SAT problems, and since binary clauses cannot be subsumed by anything other than binary clauses, the subsumption algorithm has been notably speeded up and its memory usage has been reduced. The worst part of using implicit binary clauses has been the fact that I can no longer use binary clause-sorting to find binary xor clauses, and I must resort back to Tarjan’s strongly connected component finding algorithm. This algorithm is algorithmically faster (only O(V+E) versus O(n*logn) ), but practically slower, since I need to carry it out repeatedly, and I cannot save state. Furthermore, I haven’t yet coded it down, so I am using boost’s graph algorithm, which means that I now have a dependency in CryptoMiniSat. This will eventually be corrected, but it is already causing some trouble.

In the meantime, I have been parallelising CryptoMiniSat. Funnily enough, it took me about 2 days in total to multi-thread CryptoMiniSat versus the 4 days it took to implement implicit binary clauses. Oh well.

Documenting CryptoMiniSat

SAT,

Documenting code is not always so much fun. However, in order for the code to be extended by others, documentation needs to exist. Since I conceived CryptoMiniSat as a program to be extended by others, documentation was a must. So now, after investing about 2 weeks into documentation, it is finally ready. All major classes have been documented, along with all major functions and internal data structures. The number of comment lines I added is around a thousand, all in the Doxygen format. A preliminary HTML version is available here. I hope the quality of the documentation will improve with time, and that others might correct and add more documentation as they update the program.

While documenting the code, it occurred to me that certain variable and function names were really awkward, or reflected the state of the class from an earlier version of the code. These variables and functions have been renamed, and some even removed, since they served no purpose other than making the code bigger for no reason. I have also found a number of TODOs while going through the code: sometimes I implemented things the fast way instead of the correct way, so some data structures are really strange, slow, or both. The sourcecode with all the documentation is available here, from the gitorious code repository. I will soon make a 2.6.1 release that contains not only this newly added documentation, but other additions as well.

Why programs fail

SAT, ,

I just bought the book with the title of the blogpost by Andreas Zeller. Essentially, it’s about debugging, where the author analyses the chain of program defect leading to infected program state, finally leading to program failure. I bought the book because while working with CryptoMiniSat, I have encountered so many bugs that they could fill a book.

The problem with chasing bugs in CryptoMiniSat is that SAT solvers employ a very optimised algorithm that makes a lot of decisions per second, so recording all interesting events makes for a very big dump file. I have per-module verbosity settings, so if I can narrow down what module(s) are causing the failure, there is less debug output to go through, but sometimes I still have to wade through 10-20GB dumps to see how the program state got infected.

While going through such large dumps, the following occured to me: what if we loaded all this data into a MySQL database? Some 8 years ago I had a job where I processed a large chunk of the data on all of Hungary’s phone conversations on a daily basis. Essentially, data on your phone calls are recorded in many different databases, and these must be merged to calculate your bill and to provide statistical feedback to the company. I wrote a program that processed 3million records in about 1 hour using MySQL and a number of SQL statements that spanned approx. 2-3000 lines. In other words, I am not afraid of large databases, and I think such multi-gigabyte data could easily be loaded into a MySQL database.

The goal of loading a SAT run into a MySQL database is the following: once the MySQL data is ready, a bit of PHP, graphviz and gnuplot will plot any relevant information at any point in time about the solving. In other words, we could dig this data visually, with some very interesting effects.

For example, I have been lately having problems with clause strengthening interfering with variable elimination. The idea is in theory quite simple. Variable elimination eliminates a variable and adds clauses that represent the original clauses the variable was present in. These clauses are sometimes trivial, such as:
a or b or c or !c = true
which is never added since it is satisfied whether c is true or false. So far, so good. Clause strenghtening is a method whereby clauses are shortened. For example, if there was a clause:
e or b or c = true
the solver might discover that in fact it is also true that:
e or b = true
and replace the original clause with this, since this clause is “stronger”: it poses a more stringent requirement. The way variable elimination and clause strenghtening interact is as follows. Let’s suppose we eliminate on varible e. If the above clause is strenghtened before elimination, then instead of:
a or b or c or !c = true
we might have got:
a or b or !c = true
which must be added. We actually have more clauses because of clause strenghtening! I believe nobody ever found this anomaly. To properly quantitise how this affects solving, we need to know all states of a clause, and a web interface with a MySQL backbone could help a lot with that.