Lately, I have been thinking about how to improve variable elimination. It’s one of the most important things in SAT solvers, and it’s not exactly easy to do right.

### Variable elimination

Variable elimination simply resolves every occurrence of a literal with every occurrence of the literal , removes the original clauses and adds the resolvents. For example, let’s take the clauses

When gets eliminated the resolvents become

The fun comes when the resolvents are tautological. This happens in this case for example:

The resolvent is the clause

Which contains both a literal and its negation and is therefore always true. It’s good to find variables we can eliminate without and side-effects, i.e. variables that eliminate without leaving any resolvents behind. However, it’s not so cheap to find these. Until now.

### A fast procedure for calculating the no. of non-tautological resolvents

The method I came up with is the following. For every clause where is inside, I go through every literal and in an array the size of all possible literals, I set a bit. For every clause, I set a different bit. When going through every clause of every literal where is present, I calculate the hamming weight (a popcount(), a native ASM instruction on modern CPUs) of the array’s inverse literals and substruct this hamming weight from the number of clauses was inside. I sum up all these and then the final count will be the number of non-tautological resolvents. Here is a pseudo-code:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
mybit = 1 num = 0 for clause in clauses[v1]: for l in clause: myarray[l] |= mybit mybit = mybit << 1 num += 1 count = 0 for clause in clauses[not v1]: tmp = 0 for l in clause: tmp |= myarray[not l] count += num - popcount(tmp) print "number of non-tautological resolvents: %d" % count |

I think this is pretty neat. Notice that this is linear in the number of literals in the clauses where and is present. The only limitation of this approach is that ‘myarray’ has to have enough bits in its elements to hold ‘num’ number of bits. This is of course non-trivial and can be expensive in terms of memory (and cache-misses) but I still find this approach rather fun.

Using this procedure, I can check whether all resolvents are tautological, and if so, remove all the clauses and not calculate anything at all. Since this happens very often, I save a lot of calculation.