# SAT solvers

### From Learning Logic for Computer Science

A **SAT solver** is an algorithm or a piece of software that determines 1-assignments for a given propositional formula. In many cases, SAT solvers take propositional formulas in CNF as input, see DIMACS format.

A **SAT test**, on the contrary, is an algorithm or a piece of software that determines whether a given propositional formula is satisfiable, that is, whether it has a 1-assignment or not.

# Naive SAT solver

There is a straightforward way of implementing a SAT solver.

NaiveSATSolve($\varphi$) Precondition: $\varphi$ is an arbitrary propositional formula. let $V = \text{vars}(\varphi)$ for every variable assignment $\beta \colon V \to \{0,1\}$ if $\llbracket \varphi\rrbracket_\beta = 1$ return $\beta$ return $\bot$ Postcondition: return is a 1-assignment for $\varphi$ if $\varphi$ is satisfiable; return = $\bot$ if $\varphi$ is unsatisfiable

**Proposition**
The worst case running time of the naive SAT solver is $\Omega(2^n)$ where $n$ is the number of variables in the input.

# Backtracking SAT solver

There is a very simple backtracking approach for determining a 1-assignment for a given propositional formula $\varphi$. Choose any variable that occurs in $\varphi$, say $X_i$. Then "simplify" $\varphi$ in two ways, by setting $X_i$ to $\bot$ and, dually, $X_i$ to $\top$. (These new formulas have one variable less.) Compute, recursively, (tight) 1-assignments for these two formulas. If any is found, extend it to a 1-assignment of $\varphi$ by setting $X_i$ to $0$ (if a 1-assignment was found in the first recursive call) or to $1$ (if a 1-assignment was found in the second recursive call). When no variables are left, simply evaluate the formula to see whether the empty assignment works or the formula is unsatisfiable.

**Example**
Assume $\varphi$ is defined by $\varphi = (\neg X_0 \vee X_1) \wedge X_0$. Then setting $X_0$ to $\bot$ leaves us with an unsatisfiable formula, namely $(\neg \bot \vee X_1) \wedge \bot$, whereas setting $X_0$ to $\top$ leaves us with the formula $(\neg \top \vee X_1) \wedge \top$, for which $\{X_1 \mapsto 1\}$ is a 1-assignment. Overall, $\{X_0 \mapsto 1\} \cup \{X_1 \mapsto 1\}$ is a 1-assignment for $\varphi$.

In the above argument, recursion is **not** spelled out. So, for completeness, this is explained in what follows.

Setting $X_1$ to $\bot$ in $(\neg \bot \vee X_1) \wedge \bot$ yields $(\neg \bot \vee \bot) \wedge \bot$, which evaluates to $0$; setting $X_1$ to $\top$ in $(\neg \bot \vee X_1) \wedge \bot$ yields $(\neg \bot \vee \top) \wedge \bot$, which evaluates to $0$, too.

Setting $X_1$ to $\bot$ in $(\neg \top \vee X_1) \wedge \top$ yields $(\neg \top \vee \bot) \wedge \top$, which evaluates to $0$; setting $X_1$ to $\top$ in $(\neg \top \vee X_1) \wedge \top$ yields $(\neg \top \vee \top) \wedge \top$, which evaluates to $1$, finally.

In this example, every possible option—every possible tight assignment—has to be checked, that is, the corresponding tree is a full binary tree. The same is true for every unsatisfiable formula, but for satisfiable ones, certain parts of the tree may not be explored, because a 1-assignment is encountered early in the search.

The above algorithm can be easiliy phrased in pseudocode:

BacktrackingSATSolve($\varphi$) Precondition: $\varphi$ is an arbitrary propositional formula. if vars($\varphi$) = $\emptyset$ if $\llbracket \varphi\rrbracket_\emptyset = 0$ return $\bot$ else return $\emptyset$ else let $X_i$ $\in$ vars($\varphi$) let $\varphi_0 = \varphi\{X_i \mapsto \bot\}$ let $\varphi_1 = \varphi\{X_i \mapsto \top\}$ r = BacktrackingSATSolve($\varphi_0$) if $r \neq \bot$ return $\{X_i \mapsto 0\} \cup r$ else $r$ = BacktrackingSATSolve($\varphi_1$) if $r \neq \bot$ return $\{X_i \mapsto 1\} \cup r$ else return $\bot$ Postcondition: return is a 1-assignment for $\varphi$ if $\varphi$ is satisfiable; return = $\bot$ if $\varphi$ is unsatisfiable

**Proposition**
The worst case running time of the backtracking SAT solver is $\Omega(2^n)$ where $n$ is the number of variables in the input.

# Self-reducing SAT solver

When a SAT test is given, then a SAT solver which runs in time polynomial in the formula and calls the SAT test a linear number of times on smaller formulas can be designed.

In other words, if SAT could be solved in polynomial time, then 1-assignments of satisfying formulas could be determined in polynomial time.

SelfreducingSATSolve($\varphi$) Precondition: $\varphi$ is an arbitrary propositional formula. if SATtest($\varphi$) return SelfreducingSATSolve2($\varphi$) else return $\bot$ Postcondition: return is a 1-assignment for $\varphi$ if $\varphi$ is satisfiable; return = $\bot$ if $\varphi$ is unsatisfiable SelfreducingSATSolve2($\varphi$) if $\text{vars}(\varphi) = \emptyset$ if $\varphi \equiv \bot$ return $\bot$ else return $\emptyset$ else let $X_i \in \text{vars}(\varphi)$ let $\varphi_0 = \varphi\{X_i \mapsto \bot\}$ let $\varphi_1 = \varphi\{X_i \mapsto \top\}$ if SATtest($\varphi_0$) return $\{X_i \mapsto 0\}$ $\cup$ SelfreducingSATSolve2($\varphi_0$) else return $\{X_i \mapsto 1\}$ $\cup$ SelfreducingSATSolve2($\varphi_1$)

**Proposition**
In the worst case, the self reducing SAT solver runs in time polynomial in the size of the formula and calls the SAT test at most $n+1$ times where $n$ is the number of variables in the input. Each call is on a formula which is not larger than the input formula.