SAT

also: satisfiability, boolean satisfiability

The Boolean satisfiability problem: given a propositional formula, decide whether some assignment of true and false to its variables makes it true. It is the canonical NP-complete problem, and also one that modern solvers routinely settle for instances with millions of variables.

Given a propositional formula over boolean variables, decide whether any assignment makes it true. SAT was the first problem shown NP-complete, so every problem in NP reduces to it in polynomial time, and a polynomial SAT algorithm would collapse P and NP.

The practical situation is the interesting one. Worst-case behaviour is unchanged since 1971, and yet solvers routinely decide industrial instances with millions of variables, because real instances have structure that the search exploits and adversarial ones do not.

Solvers take input in conjunctive normal form, a conjunction of disjunctions:

The form is chosen because the two facts a solver needs are immediate in it: a clause with every literal false is a conflict, and a clause with exactly one unassigned literal forces that literal. Converting an arbitrary formula preserves satisfiability at linear cost by the Tseitin transformation, which names each subformula with a fresh variable rather than distributing out to an exponentially larger equivalent.

DPLL · CDCL

• Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.