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.