The Boolean Satisfiability problem (SAT) is an NP-Complete problem of deep theoretical importance to the world of Computer Science. The problem takes a Boolean expression (comprised of and (∧), or (∨), and not (¬) operators and variables as input, and seeks to find an assignment to variables that makes the expression evaluate to True.
One of the most common forms of the SAT problem is CNF satisfiability. In CNF satisfiability a clause is a statement comprised of variables joined together by or operators. E.g., (¬a ∨ c ∨ d).
A full formula, φ, in conjunctive normal form (CNF), is a conjunction (and) of clauses.
E.g.,
φ = (a ∨ b) ∧ (¬a ∨ c ∨ d) ∧ (¬b ∨ ¬d)
is a valid expression in CNF form.
Software designed to solve Satisfiability problems are know as SAT solvers.
Given the formula φ above, we can satisfy the formula:
a = True,b = False,c = True, andd = True.
Note that this is not the only satisfying assignment to φ.
Note that identifying a satisfying valuation to φ is fairly straight-forward. Due to the nature of the or operator, any assignment that is included in a clause satisfies the clause, and an assignment that satisfies each individual clause satisfies the entire expression.
E.g., The clause (a ∨ b) is satisfied by a = True, (¬a ∨ c ∨ d) is satisfied by either c = True or d = True, and (¬b & or; ¬d) is satisfied by b = False.
Note that since this example instance was designed to be satisfiable, both the sat.lp and max-sat.lp programs will generate satisfying instances, with the latter annotating that all clauses are satisfied, and displaying any relevant optimization information.
Satisfiability, logic, and logic programming are active areas of research with many possible problem variations.
The 2-Satisfiability problem is a special case of CNF Satsifiability where clauses are limited to length 2. Unlike more general versions of CNF-SAT, 2-SAT is NL-Complete, and can be solved in Polynomail time.
The 3-Satisfiability problem is a special case of CNF SAT where clauses are limited to length 3. Unlike 2-SAT, and like unrestricted CNF Satisfiability, 3-SAT is NP-Complete, and the only known algorithms that solve it run in exponential time in the worst case.
3-SAT is also universal--given a propositional SAT instance comprised of any operators applied in a consistent manner we can convert the instance to an equivalent instance of 3-SAT.
The Maximum Satisfiability problem (MAX-SAT) is a generalization of the CNF Satisfiability problem. MAX-SAT allows unsolved clauses, and instead seeks to maximize the number of clauses that evaluate to True. This problem is in NP-Hard, making it more difficult to solve in practice than most other variants named here.
Many other forms of SAT exist, like Disjuntive Normal Form (DNF-SAT), which switches the roles of and and or operations.
While this repository explores many problems of historical and theoretical importance, Boolean Satisfiability serves an important role in the history of theoretical and applied Computer Science.
The Cook–Levin theorem established that Boolean Satisfiability is NP-Complete, the first such problem to be identified in the class. Not long after, Richard Karp used this result to locate the the first 21 NP-Complete Problems. This list included 3-SAT, which was used to demonstrate that a number of other problems were NP-Complete.
While SAT solvers were an active area of research for decades prior, the late 1990s and early 2000s saw a significant advancement in the state of the art--technology that would later pave the way for modern Answer Set Programming languages such as Clingo.