All posts by msoos

Hyper-binary resolution: I was wrong, again

SAT,

I am not perfect, so I make mistakes. One of the more memorable mistakes I have made has been regarding hyper-binary resolution. More specifically, in this post I wrote that I cannot add as many binary clauses using hyper-binary resolution as Armin Biere, one of the leading SAT solver experts, and I proposed a reason that would have meant that CryptoMiniSat was doing things differently and thus better. Well, I was wrong, on multiple accounts.

First of all, there was an awful bug in the code that meant that hyper-binary resolution was not carried out on negated variables. Second, when it was decided that multiple implications need to be attached to a literal, I didn’t check for redundancy. For example, if v1 had to be connected to v2 and v3, I simply added the clauses
-v1 OR v2 (1)
-v1 OR v3 (2)
However, this may not be very efficient, since if there is already a binary clause
-v2 OR v3 (3)
then clause (2) doesn’t need to be added. The added redundant binary clauses reduced the speed of solving while adding no extra knowledge. There were many of them, too: approx 2/3rd of all binary clauses added were redundant.

Hyper-binary resolution is conceptually not too difficult, but takes a lot of thinking to code efficiently, is very time consuming and its benefits are not clear-cut. I believe the problem is that many binary clauses added this way are ultimately useless, since most are connected to variables that will soon be proved to be of a fixed value. Another possibility is that since problems are pretty structured, and it’s usually best to attack problems in a specific way (which is normally correctly guessed by the VSIDS and polarity-guessing&caching heuristics), the binary clauses added by hyper-binary resolution do not help resolving the problem given the (typically correct) attack method employed by SAT solvers. In other words, the information added is nice, but mostly unused. This is just wild speculation, and I may only think this because my code is slow — I believe Armin’s code is faster, so I should have a look.

Dependent Literals

SAT

I have lately been trying to work on branching heuristics. The idea is relatively simple. If we have a cache of what propagates what, we can try to branch on literals that propagate a lot of other literals. The algorithm boils down to the following:

  1. For each literal L, we select a literal DL that propagates L and has the largest tree of propagated literals.. We call this DL the dominating literal. Naturally, some literals don’t have a dominating literal, and some literals appear as dominating literals for many other literals.
  2. When branching, if we are supposed to branch on a literal that has a dominator, we pick the dominator instead of the literal. This not only ensures that the literal will be set, but it will probably also set a number of other literals.
  3. Using the heuristic of step 2, we should reach a conflict earlier, with less decisions taken. This should lead to faster conflicting, and thus faster solving.

Of course things aren’t as simple as they seem. First of all, as George has indicated to me, Jarvisalo and Junttila have published  a paper entitled Limitations of restricted branching in clause learning, which deals with issues related to this branching heursitic. The baseline of that paper is that it’s a bad idea to branch only on dependent (they call them input) variables. I haven’t really got very deep into this, but there are some subtle differences between the heuristic above and dependent variables, notably that I have treated dependent literals above, while Matti and Tommi are treating dependent variables.

As for the advantages of the above heuristic, it seems to work on some instances in practice. In particular, it allows me to solve some cryptographic instances significantly faster — in fact, some instances that have been extremely hard to solve are now solveable. To me, this looks like an indication that the heuristic is not entirely useless. There are some subtle problems, but it seems that a mixture of randomly branching either on the literal or on its dominator fixes most problems. Indeed, I think CryptoMiniSat 3.0.0 will be released with this experimental feature turned on by default.

PS: CryptoMiniSat 3.0.0 is coming soon, I believe. It’s going to provide a fully multi-threaded library&executable, with a MiniSat-compatible syntax, so anyone will be able to multi-thread his or her SMT solver at a whim.

Caching

SAT, , ,

“Representation is the essence of programming”
Frederic P. Brooks Jr., “The Mythical Man-month”

Looking through the literature on SAT solvers, it is rare to find any algorithm that uses a form of time-memory trade-off. In fact, it is rare to find any algorithm that uses too much memory. This also shows up in practice, as it’s rare to find a SAT solver using too much memory. This translates to the following: if a SAT solver can in an effective way utilize the typically abundant memory, that SAT solver will have an advantage. Based on this logic, I think CryptoMiniSat is doing good.

What I have realised is that it’s great to know all the literals we can reach from any given literal. Let me explain. Let’s say we have a look at literal “v1”, i.e. “v1 = true”. We propagate this literal as usual, and we reach a set of literals that are implied. For example, we reach “v2, v3, -v4”. This knowledge is regularly computed by modern SAT solvers, but is also quickly thrown away. I advocate keeping this, and here is why. There are a number of very interesting things we can do with these, three of which I have found useful.

Number one. This is the best, and the least obvious one. The algorithm used for computing equivalent literals (i.e. “v1 = -v2” or “v1 = v4”) is a variation of Tarjan’s algorithm for finding strongly connected components (SCC). This algorithm requires a set of binary clauses such as “-v1 v2” and “v1 -v2” as input to find equivalent literals, in the example case “v1 = -v2”. The most obvious way to “feed” this algorithm with information is to give it all the binary clauses we have. But that misses out on all the binary clauses that are not directly apparent in the problem, but  could be derived from the problem. For example, if “-v1 -v4” was not directly in the problem, SCC cannot find the equivalence “v1 = v4”. Naturally, by using our cache, we can be sure that “-v1 -v4” is part of the problem (since “v1” propagates “-v4”). So, using this cache, we can substantially increase the power of SCC. More equivalent literals lead to less variables, and an overall faster solving.

Number two. Clause vivification is a method to make the original clauses of the problem shorter. It’s a relatively simple algorithm that enqueues the literals in the clauses one-by-one and checks if their propagation leads to a conflict. If so, then the clause can be shortened. With the cache, we can do something similar, though less powerful in terms of reasoning power, but far more effective in terms of speed. The trick is to simply try every single literal in the clause: if a literal propagates the inverse of another literal in the clause, we can remove it. For example, if the clause is “a b -c”, and in the cache for “b” there is “f,g,h,j,-c”, then we know that conceptually there exists a clause “-b -c”, which means we can now remove “b” from the original clause, using the the self-subsuming resolution rule. This form of vivification is, although technically less strong than normal vivification, is typically 50-100x faster than normal vivification and is almost as powerful. This kind of speed advantage means it can essentially be carried out without (time) penalty.

Number three. When generating conflict clauses, MiniSat-type conflict minimisation has now become commonplace. This uses the clauses involved in the conflict to carry out self-subsuming resolution on the conflict clause generated. Just as with clause vivification, we can use our cache to carry out self-subsuming resolution with the (conceptually binary) clauses stored in the cache. This is not much different from clause vivification, but it allows us to do simplification in the middle of a restart, instead of patiently waiting for the restart to end. Furthermore, it can uncover that certain learnt clauses can become binary, thus alleviating the problem of cleaning “useless” learnt clauses that could have become binary through, e.g. clause vivification.

I am aware that all the above three could be carried out without a cache — in fact, CryptoMiniSat could do (and most of the time did) all of the above without it. The advantage of having the cache is speed: things that used to take immense amounts of time can now be done really fast. However, what interests me the most in this cache, is the new uses that will come of it. I was originally only aware of number (3), then when I realised (1), I dived deep and realised that (2) can be done. I think more uses will eventually emerge.

The Cathedral

SAT,
Cathedral of Transfiguration in Habarovsk (picture credit: paukrus)

Last week I visited Micosoft Reasearch in Cambridge, where I gave a talk on SAT solvers, Grobner basis algorithms, and Cryptography. It was nice to visit Microsoft, and in particular I enjoyed seeing how “the cathedral” works. The kind of software development carried out at Microsoft and almost all large software companies is called the cathedral model due to the book “The Mythical Man-Month“. It’s a very interesting book that talks about how software (and in particular, a “Programming Systems Product”) is developed. All Windows variants, and e.g. the IBM System/360 fall into the category of programming systems products: they are all tested, documented, extensible, have predefined inputs and outputs, come with predefined interfaces, etc. The development of these software is called the cathedral model simply because that’s the example the book uses, and it got stuck in the literature.

I have been developing CryptoMiniSat for quite some while now, and I must say it is exceedingly difficult to create a programming systems product — CryptoMiniSat doesn’t even scratch the surface of the requirements, but then almost no SAT solver does — maybe SAT4J is the sole exception. Documentation is usually scarce, and even though I have added a lot, it’s still not enough. The input is rarely checked for sanity, and resource needs are usually just ignored: if memory is not enough, then the program will probably just crash; don’t expect graceful degradation.

As for Microsoft, I must say I was pretty impressed. It’s a nice building, with large offices, free tea/coffee/orange juice, filled with some very kind and very bright people. The audience was astonishingly good too, asking questions when they felt like they haven’t understood something, instead of just getting disinterested and e.g. browsing email. All in all, it was very interesting to visit the place, though I still feel more inclined to release my code as Free Software ;)

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.