Satisfiability

Satisfiability, in the context of propositional logic, is the question of whether a given Boolean formula can be assigned truth values to its variables so that the formula evaluates to true. In practice, formulas are often written in conjunctive normal form (CNF), a conjunction of clauses where each clause is a disjunction of literals (a variable or its negation). The decision problem asks whether such an assignment exists; if so, the formula is satisfiable (SAT); if no assignment can satisfy all clauses, it is unsatisfiable (UNSAT). A common restricted form is k-SAT, where each clause contains at most k literals; 3-SAT is a well-studied nontrivial case.

Satisfiability is a central topic in computational complexity. It was shown to be NP-complete by the Cook-Levin theorem, establishing that every problem in NP can be reduced to SAT in polynomial time. This result links logic with computational intractability and positions SAT as a canonical hard problem. Many computational problems in verification, planning, and artificial intelligence can be reduced to SAT or to SAT modulo theories (SMT), which extend SAT with arbitrary theories.

Algorithmically, practical SAT solving combines theoretical insight with engineering. The Davis–Putnam–Logemann–Loveland (DPLL) framework underpins many solvers, augmented by conflict-driven clause learning (CDCL), non-chronological backtracking, and heuristics. There are also local-search methods, such as WalkSAT, which can solve hard random instances efficiently in practice. Some specialized forms, like Horn-SAT or 2-SAT, are solvable in polynomial time.

Applications of SAT solvers span hardware and software verification, model checking, cryptography, theorem proving, scheduling, and constraint solving, making satisfiability a foundational concept in computer science.