# A variable elimination improvement

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:

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.