SAT solvers

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.