A variable elimination improvement | Wonderings of a SAT geek

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 $v1$ with every occurrence of the literal $\neg v1$ , removes the original clauses and adds the resolvents. For example, let’s take the clauses

$v1 \vee v2 \vee v3$
$v1 \vee v4 \vee v5$
$\neg v1 \vee v10 \vee v11$
$\neg v1 \vee v12 \vee v13$

When $v1$ gets eliminated the resolvents become

$v2 \vee v3 \vee v10 \vee v11$
$v2 \vee v3 \vee v12 \vee v13$
$v4 \vee v5 \vee v10 \vee v11$
$v4 \vee v5 \vee v12 \vee v13$

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

$v1 \vee v4$
$\neg v1 \vee v5\vee \neg v4$

The resolvent is the clause

$v4 \vee \neg v4 \vee v5$

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 $v1$ 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 $\neg v1$ 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 $v1$ 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:

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 $v1$ and $\neg v1$ 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.