How SAT Solver works
This is a summary over the high-level design of SAT solver covered in Prof. Dillig’s Automated Logical Reasoning class. It’s meant to cover the basic steps towards determining whether a given boolean formula is satisfiable or not.
Convert to NNF
The first step in a SAT solver is to convert a given boolean formula to Negation Normal Form (NNF). A normal form of a formula \(F\) is another formula \(F’\) such that \(F\) is equivalent to \(F’\), but obeys certain syntactic restrictions. NNF has two syntactic restrictions:
- The only logical connectives are \(\neg\), \(\land\), and \(\lor\).
- Negation appears only in literals. (i.e., no \(\neg(a \land b)\)).
Why not DNF?
A formula in disjunctive normal form (DNF) is a disjunction of conjunction of literals. It can be expressed as:
\[ \begin{equation} \bigvee_i \bigwedge_j l_{i,j} \mbox{ for literals }l_{i,j} \tag{1} \end{equation} \]
That formula states that \(\lor\) can never appear inside \(\land\) or \(\neg\). If we take a look at formula in DNF, we might claim it’s trivial to determine satisfiability of such formula. This is because, if we can find one element that evaluates to true, then due to the nature of \(\lor\), it must be that the formula evaluates to true.
Practically, this is impractical. This is because DNF conversion causes exponential blow-up in size. Take formula \((F_1 \land F_2) \land (F_3 \lor F_4)\) for example, the DNF will become \((F_1 \land F_3) \lor (F_1 \land F_4) \lor (F_2 \land F_3) \lor (F_2 \land F_4)\). The main problem is distributing \(\lor\) over \(\land\) will introduce more elements to the formula.
CNF
The solution is to convert from NNF to conjunctive normal form (CNF). CNF is a conjunction of disjunction of literals:
\[ \begin{equation} \bigwedge_i \bigvee_j l_{i,j} \mbox{ for literals }l_{i,j} \tag{2} \end{equation} \]
What this says that \(\land\) is not allowed inside \(\lor\) and \(\neg\), or clauses.
CNF vs DNF
Unlike CNF, it is not trivial to determine satisfiability of formula in CNF. However, it is just as expensive to convert formula to CNF as to DNF. So why do most solvers convert to CNF although it’s easier to determine satisfiability in DNF?
Tseitin’s Transformation
The answer is Tseitin’s Transformation. The most important thing about Tseitin’s Transformation is that it converts formula \(F\) to equisatisfiable formula \(F’\) in CNF with only a linear increase in size.
Tseitin’s Transformation has three major steps:
- Introduce a new variable \(p_G\) for every subformula \(G\) of \(F\).
- Consider each subformula \(G : G_1 \circ G_2\), stipulate representative of \(G\), or that \(p_G \leftrightarrow p_{G_1} \circ p_{G_2}\).
- Convert \(p_G \leftrightarrow p_{G_1} \circ p_{G_2}\) to CNF.
Eventually, we will introduce a new formula:
\[ \begin{equation} p_F \bigwedge_{(G=G_1\circ G_2)\in S_F} CNF(p_g \leftrightarrow p_{g_1} \circ p_{g_2}) \tag{3} \end{equation} \]
Precisely, the size of resulting formula is bound by \(30n + 2\) where \(n\) is the size of original formula.
DPLL
The Davis-Putnam-Logemann-Loveland (DPLL) algorithm can be expressed as:
BCP stands for boolean constraint propagation. It requires that one of the clauses must be a unit clause. Performing BCP (or unit resolution) is same as replacing a literal with true in the original clauses.
choose_variable contains multiple heuristics. For now we can consider a variable is randomly picked.
The red part is optimization to the original DPLL. Pure literal Propagation (PLP). All it does is if variable \(p\) occurs only appears only in the form of \(p\) or \(\neg p\) in the entire formula, we will set all occurences of \(p\) or \(\neg p\) to true or false.