$$ $$ $$ $\text{usepackage}pifont$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $\text{You can't use 'macro parameter character \#' in math mode}$ $$ $\text{You can't use 'macro parameter character \#' in math mode}$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

$$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

Preprocessing

Unit clause propagation is relatively efficient in pruning the search space and it can be implemented to work very efficiently by using proper data structures. Thus many SAT solvers use it, and only it, as the constraint propagation technique during the search. However, there are other techniques that could prune the search space in different ways but are considered to be too slow to be used in the inner loop of the search. One alternative for applying such techniques is to use them for preprocessing the formula before the search phase. That is, given a CNF fomula $\varphi$, they are applied to construct another formula ${\varphi }^{\prime }$ such that

• ​ $\varphi$ is satisfiable if and only if ${\varphi }^{\prime }$ is,

• ​ from a model of ${\varphi }^{\prime }$, it is possible to reconstruct a model for $\varphi$, and

• ​ ${\varphi }^{\prime }$ is (hopefully) easier to solver that $\varphi$.

Thus they can be seen as transformations that preserves satisfiability and the process of SAT solving with preprocessing is as follows:

In the CDCL approach, such techniques can also be used interleaved with the search after restarts — in this case, one speaks about “inprocessing”.

In the following, we give examples of some simple preprocessing techniques. Please see, for instance, these slides by Marijn Heule for some other techniques used in modern SAT solvers as well.

Pure literal elimination

A literal $l$ occurring in a CNF formula $\varphi$ is pure if the negated literal $\mathrm{\neg }l$ does not occur in $\varphi$. If $l$ is pure in $\varphi$, then it is quite easy to see that if $\tau =\{\mathrm{\neg }l,...\}$ satisfies $\varphi$, then so does ${\tau }^{\prime }=(\tau \setminus \{\mathrm{\neg }l\})\cup \{l\}$. Therefore, if $l$ is pure in $\varphi$, one can simplify $\varphi$ by setting $l$ to true and removing all the clauses in which $l$ occurs. This is called a pure literal elimination step. The resulting formula is satisfiable if and only $\varphi$ is. Observe that removing clauses can make new pure literals. The pure literal elimination process repeats the pure literal elimination step until the formula no longer has any pure literals.

Example: Pure literal elimination

Consider the formula

$$\varphi =(a\vee \mathrm{\neg }c\vee \mathrm{\neg }d)\wedge (\mathrm{\neg }b\vee c)\wedge (a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }a\vee b\vee c)\wedge (\mathrm{\neg }a\vee b).$$

The literal $\mathrm{\neg }d$ is pure in $\varphi$. After removing all the clauses with it we get

$${\varphi }_1=(\mathrm{\neg }b\vee c)\wedge (a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }a\vee b\vee c)\wedge (\mathrm{\neg }a\vee b).$$

Now the literal $c$ is pure and we get the simplified formula

$${\varphi }_2=(a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }a\vee b).$$

The truth assignment ${\tau }_2=\{a,b\}$ satisfies the simplied formula ${\varphi }_2$. Inserting the removed pure literals, we get the truth assignment $\tau =\{a,b,c,\mathrm{\neg }d\}$ that satisfies the original formula $\varphi$.

Blocked clause elimination

Blocked clause elimination [Kullmann1999] is another method for removing “redundant” clauses in a satisfiability-preserving way. We say that a clause $C$ in a CNF formula $\varphi$ is blocked if $C$ contains a literal $l$ such that, for all other clauses $D$ in $\varphi$, it holds that if $D$ contains $\mathrm{\neg }l$, then $D$ also contains another literal $p$ such that $C$ contains $\mathrm{\neg }p$. In such a case, we say that $l$ blocks $C$ in $\varphi$, and $l$ is a blocking literal of $C$ in $\varphi$.

Theorem

If $C$ is blocked in $\varphi$, then $\varphi$ is satisfiable if and only if $\varphi \setminus \{C\}$ is satisfiable.

Proof sketch

If a truth assignment $\tau$ satisfies $\varphi$, then $\tau$ also satisfies $\varphi \setminus \{C\}$ because it satisfies all the clauses in $\varphi$ and thus in $\varphi \setminus \{C\}$.

In the other direction, assume that an assignment $\tau$ satisfies $\varphi \setminus \{C\}$ but not $\varphi$. Thus $\tau$ satisifes all the clauses in $\varphi$ except $C$. Suppose that the blocking literal of $C$ is $l$. Thus $\tau$ must evaluate $l$ to false. Let ${\tau }^{\prime }$ be the assignment similar to $\tau$ except that it evaluates $l$ to true. Now ${\tau }^{\prime }$ satisfies $\varphi$. We can argue this as follow. Firstly, ${\tau }^{\prime }$ satisfies all the clauses in $\varphi$ that do not involve $l$ or $\mathrm{\neg }l$ because $\tau$ does. Secondly, ${\tau }^{\prime }$ obviously satisfies all the clauses in $\varphi$ that contain the literal $l$. Finally, ${\tau }^{\prime }$ satisfies all the clauses $D$ in $\varphi$ that contain the literal $\mathrm{\neg }l$ because ${\tau }^{\prime }$ evaluates all the other literals except $l$ in $C$ to false and $D$ must contain the negation of one of these literals by the definition of blocked clauses.

Thus one may remove a blocked clause from $\varphi$ and preserve satisfiability. Observe that if a clause contains a pure literal $l$, then the clause is blocked because no other clause contains the negated literal $\mathrm{\neg }l$. Thus blocked clause elimination is stronger than pure literal elimination in the sense that it can remove all the clauses that pure literal elimination can and, in many cases, many others as well.

Example

Consider the CNF formula

$$\varphi =(a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }a\vee b)\wedge (a\vee b\vee c)\wedge (\mathrm{\neg }b\vee \mathrm{\neg }c)$$

Observe that the formula has no pure literals and thus pure literal elimination cannot remove any clauses from it. However:

1. The clause $(a\vee \mathrm{\neg }b)$ is blocked because for the literal $a$ in it, only the clause $(\mathrm{\neg }a\vee b)$ contains $\mathrm{\neg }a$, and $(\mathrm{\neg }a\vee b)$ contains the lietral $b$ and $(a\vee \mathrm{\neg }b)$ contains the literal $\mathrm{\neg }b$. We can thus remove the clause $(a\vee \mathrm{\neg }b)$ and get the formula

   $${\varphi }_1=(\mathrm{\neg }a\vee b)\wedge (a\vee b\vee c)\wedge (\mathrm{\neg }b\vee \mathrm{\neg }c)$$

2. Now the clause $(a\vee b\vee c)$ is blocked because for the literal $b$ in it, the clause $(\mathrm{\neg }b\vee \mathrm{\neg }c)$ with $\mathrm{\neg }b$ contains $\mathrm{\neg }c$ and $(a\vee b\vee c)$ contains its negation $c$. Removing this blocked clause gives the formula

   $${\varphi }_2=(\mathrm{\neg }a\vee b)\wedge (\mathrm{\neg }b\vee \mathrm{\neg }c)$$

3. The clause $(\mathrm{\neg }a\vee b)$ is now blocked due to the (pure) literal $\mathrm{\neg }a$ and we get the formula

   $${\varphi }_3=(\mathrm{\neg }b\vee \mathrm{\neg }c)$$

4. Now $(\mathrm{\neg }b\vee \mathrm{\neg }c)$ is blocked because of the (pure) literal $\mathrm{\neg }c$ and, by removing it, we get the trivially satisfiable empty formula.

As the last formula is satisfiable, the original formula is satisfiable as well.

Let’s reconstruct a satisfying truth assignment for the original formula by using the construction described in the proof above. We start from the last formula and select an arbitrary satisfying truth assignment for it; however, we also assign arbitrary values for the variables that appear in the original formula as well. Suppose that we pick the truth assignment ${\tau }_1=\{\mathrm{\neg }a,\mathrm{\neg }b,\mathrm{\neg }c\}$ assigning all the variables to false.

1. The clause $(\mathrm{\neg }b\vee \mathrm{\neg }c)$ was the last one that was removed, due to the blocking literal $\mathrm{\neg }c$. The assignment ${\tau }_3$ satisfies the clause $(\mathrm{\neg }b\vee \mathrm{\neg }c)$ and thus the formula ${\varphi }_3=(\mathrm{\neg }b\vee \mathrm{\neg }c)$ as well.

2. The clause $(\mathrm{\neg }a\vee b)$ was then the previous one removed, due to the blocking literal $\mathrm{\neg }a$. The assignment ${\tau }_2={\tau }_3$ satisties $(\mathrm{\neg }a\vee b)$ as well and thus also the formula ${\varphi }_2=(\mathrm{\neg }a\vee b)\wedge (\mathrm{\neg }b\vee \mathrm{\neg }c)$.

3. The clause $(a\vee b\vee c)$ was removed due to the blocking literal $b$. The assignment ${\tau }_2$ does not satisfy the clause and thus we flip the value of the blocking literal $b$ and obtain the assignment ${\tau }_1=\{\mathrm{\neg }a,b,\mathrm{\neg }c\}$. Now ${\tau }_1$ satisfies not only the clause $(a\vee b\vee c)$ but also the clauses in the formula ${\varphi }_2$. Therefore, it satisfies the formula ${\varphi }_1=(\mathrm{\neg }a\vee b)\wedge (a\vee b\vee c)\wedge (\mathrm{\neg }b\vee \mathrm{\neg }c)$ as well.

4. Finally, ${\tau }_1=\{\mathrm{\neg }a,b,\mathrm{\neg }c\}$ does not satisfy the first removed blocked clause $(a\vee \mathrm{\neg }b)$. Thus we flip the value of the blocking literal $a$ and get the assignment $\tau =\{a,b,\mathrm{\neg }c\}$. This assignment satisfies the clause and all the clauses in ${\varphi }_1$ and thus the original formula $\varphi$ as well.