SAT Solvers for CNF Formulas: common preliminaries
Recall that a SAT solver is an algorithm/tool that takes as input a propositional formula and then finds out whether the formula is satisfiable or not.
After providing some common preliminary definitions below, we will learn the fundamentals of how most modern SAT solvers work:
In the section The DPLL backtracking search procedure, we review the classic, basic DPLL search procedure for solving satisfiability.
In Conflict-driven clause learning (CDCL) SAT solvers, we see how that basic search procedure is extended with a reasoning technique that allows learning from mistakes.
In the section Preprocessing, we see some basic techniques for simplifying the formula before the search phase.
Finally, in the section The resolution proof system we introduce the classic method for producing machine-verifiable proofs of unsatisfiability.
Observe that we will omit several crucial parts needed to make SAT solvers to really work in practise. Some links to extra material explaining these aspects are provided in the relevant sections.
Partial truth assignments
The DPLL and CDCL search procedures for SAT both try to build a satisfying truth assignment incrementally, heuristically extending a truth assignment for some subset of the variables to a larger subset. This is continued until a satisfying truth assignment is found or some clause is falsified. In the former case, the search ends in the verdict “the formula is satisfiable”. In the latter case, the algorithms backtrack by removing some parts of the assignment and then continue the search with different assignment values. We next introduce some notation and definitions used in expressing such search procedures.
Given a CNF formula \(\phi\) over a set \(\VarsOf{\phi}\) variables, a partial truth assignment for it is a function \(\TA : X \to \Set{\False,\True}\) for some subset \(X \subseteq \VarsOf{\phi}\).
If \(y \notin X\), then the value of \(y\) is undefined in \(\TA : X \to \Set{\False,\True}\).
As earlier, for a negation \(\Neg{x}\) of a variable \(x \in X\), \(\TA(\Neg{x}) = \False\) when \(\TA(x) = \True\) and \(\TA(\Neg{x}) = \True\) when \(\TA(x) = \False\).
For convenience, we often see a partial truth assignment \(\TA\) as the set of literals
\[\Setdef{x}{x \in X\text{ and }\TA(x) = \True} \cup \Setdef{\Neg{x}}{x \in X\text{ and }\TA(x) = \False}\]Observe that such a set can never contain a variable and its negation. Using this set notation for truth assignments, one can use the standard set operations to build new truth assignments.
A clause \((l_1 \lor ... \lor l_k)\) is
satisfied by \(\TA\) if \(\TA(l_i) = \True\) for at least one \(i \in [1..k]\)
falsified by \(\TA\) if \(\TA(l_i) = \False\) for all \(i \in [1..k]\)
A CNF formula \(\phi\) is satisfied by \(\TA\) if \(\TA\) satisfies all the clauses in \(\phi\).
Example
A partial truth assignment \(\TA = \Set{a \mapsto\False, d \mapsto\True, e\mapsto\False}\)
In the set-of-literals notation: \(\TA = \Set{\Neg{a},d,\Neg{e}}\)
The value of \(b\) is undefined in \(\TA\)
The clause \((b \lor \Neg{c} \lor d)\) is satisfied by \(\TA\)
The clause \((a \lor \Neg{d})\) is falsified by \(\TA\)
The clause \((a \lor \Neg{b} \lor c)\) is neither satisfied nor falsified by \(\TA\)
\(\TA \cup \Set{\Neg{b}}\) means the truth assignment \(\Set{a \mapsto\False, b\mapsto\False, d \mapsto\True, e\mapsto\False}\)
Unit clause propagation
The DPLL and CDCL search procedures are always incorporated with a constraint propagation technique called “unit clause propagation” (or “unit propagation” for short). In general, “constraint propagation” means that we study the constraints (clauses in this case) under the current partial solution candidate (partial truth assignment in this case) and try to deduce new facts that help in pruning the search space.
Assume a CNF formula \(\phi\) and a partial truth assignment \(\TA\). A clause \(C =(l_1 \lor ... \lor l_k)\) in \(\phi\) is a unit clause under \(\TA\) (or simply unit) if \(\TA\) evaluates all the literals in it to false except for one literal whose value is undefined in \(\TA\). Formally, \(C\) is unit if
\(\TA(l_j)\) is undefined for some \(j \in [1 .. k]\), and
\(\TA(l_i) = \False\) for all \(i \in [1..k]\) with \(i \neq j\).
In such a case, we say that \(l_j\) is implied by \(C\) and \(\TA\) and may extend \(\TA\) to \(\TA \cup \Set{l_j}\). This step is called a unit clause propagation step and it preserves all the satisfying truth assignments: if there is a satisfying truth assignment that is an extension of \(\TA\), then it is also an extension of \(\TA \cup \Set{l_j}\). The reason for this is simple: extending \(\TA\) with \(\neg l_j\) would make the clause \(C\) falsified and thus \(\TA \cup \Set{\neg l_j}\) cannot be extended to any satisfying truth assignment.
Example
Consider the CNF formula \((a \lor \neg b) \land (a \lor c \lor \neg d) \land (\neg c \lor \neg e) \land (\neg c \lor e) \land (c \lor d)\).
In the truth assignment \(\TA = \Set{\neg a}\), the clause \((a \lor \neg b)\) is unit and we can extend \(\TA\) to \(\Set{\neg a, \neg b}\).
On \(\TA = \Set{\neg a,\neg b,\neg c}\), the clause \((a \lor c \lor \neg d)\) is unit and we can extend \(\TA\) to \(\Set{\neg a, \neg b,\neg c,\neg d}\). Now the clause \((c \lor d)\) is falsified.
Observe that a single unit propagation step can
make some other clause falsified, or
make some other clauses unit so that further unit propgation is possible.
The unit clause propagation (or simply unit propagation) is the process of applying unit clause propagation steps until (i) a clause becomes falsified, or (ii) there are no unit clauses. Given a CNF formula \(\phi\) and a partial truth assignment \(\TA\), we use \(\PseudoUP(\phi, \TA)\) to denote a partial truth assignment produced by applying the unit propagation process on \(\TA\). Observe that \(\PseudoUP(\phi, \TA)\) is (i) uniquely defined when the resulting truth assignment does not falsify any clauses but (ii) can have different outcomes when the resulting truth assignments falsify some clauses because the propagation order between different unit clauses is not defined and we stop propagation when a clause becomes falsified.
Example
Consider a CNF formula
Let us apply unit propagation on the partial truth assignment \(\TA = \Set{\Neg{a}}\).
First, \(b\) is implied by \((a \lor b)\) and we set \(\TA = \Set{\Neg{a}, b}\).
Now \(\Neg{c}\) is implied by \((a \lor \Neg{b} \lor \Neg{c})\) and we set \(\TA = \Set{\Neg{a}, b, \Neg{c}}\).
But now \(\TA\) falsifies the clause \((\Neg{b} \lor c)\) and the propagation stops.