All SAT solvers must have a tri-state class that can hold the values `true`, `false`, and `undefined`. Although it’s not hard to write code to represent such a class, it’s hard to write such it so that all typical operations are fast. In this blog post I will compare three different ways of doing it.

The original MiniSat 2.0 code

The original MiniSat 2.0 used the following code for such a class:

changed the code to the following:

lbool operator^(const bool b) const
{
  //return b ? lbool(-value) : lbool(value);
  return lbool(value * (-2*(char)b + 1));
}

This makes ‘extensive’ use of the ALU of the chip for the flip operator to avoid using the branch instruction. However, it keeps other operators cheap as per the first version. Let’s call this solution to the problem solution (3).
Comparison
I have tried to solve two different problems from the SAT Competition of 2009 with all three solutions. First is a typical electronic engineering problem, 9dlx_vliw_at_b_iq2.cnf. The second is a typical cryptographic problem, mizh-md5-47-3.cnf. Here are the timing results for my i7-3612QM (Ivy Bridge):


Problem
Solution(1)
Solution(2)
Solution(3)


9dlx_vliw_at_b_iq2.cnf
135.9s
138.8s
132.5s


mizh-md5-47-3.cnf
60.7s
60.5s
56.3s


So, in this very small test, solution(3) wins. 
And now for a bit of history. I have tried the trick in solution(3) about 3 years ago. Back then it seemed slower to perform the numerical trick than to use the branch. It turns out that on modern CPUs either the ALU is faster, branch misprediction is more costly, or both (or, the compilers have evolved to compile my numerical trickery into some weird thing). Anyway, it’s kind of a cool speedup for a one-liner.