Boolean satisfiability problem
In plain wordsThe puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions.
The decision problem of whether a propositionalpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true. formula, usually given in conjunctive normal form (an AND of clauses, each an OR of literals), is satisfiable — true under at least one assignment of truth values — with solvers also returning such an assignment. By the Cook–Levin theorem it was the original NP-completeNP-complete, adj.: Describes problems, such as solving giant Sudokus, where a proposed answer is quick to check but no known method finds one quickly; a fast method for any one of them could be turned into one for all. problem: every problem in NP reduces to it, and no algorithm is known that handles all instances in polynomial time. 3-SAT remains NP-complete, while 2-SAT is solvable in linear time. Practical solvers descend from the DPLL backtracking procedure and, since the late 1990s, use conflict-driven clause learning (CDCL), which analyzes each dead end to add a clause that prunes future search, combined with watched literals, restarts and activity-based branching heuristicsheuristic, n.: A rule of thumb: a quick, usually good-enough way to make a decision or to estimate how close you are to a goal, without any guarantee of finding the best answer.. They routinely solve industrial instances with millions of variables and are workhorses of hardware and software verification, automated planningautomated planning, n.: The branch of AI that works out a sequence of actions to reach a goal, such as the steps a robot must take to assemble a part, from descriptions of what each action needs and what it changes., scheduling, cryptanalysis and combinatorial mathematics.
We encoded the timetable as 2 million clauses and the SAT solver found a schedule in under a minute.
Origin
Stephen Cook proved SAT NP-complete in 1971, independently of Leonid Levin (published 1973). Martin Davis and Hilary Putnam's 1960 procedure, refined with George Logemann and Donald Loveland in 1962 (DPLL), founded practical solving; CDCL came from João Marques-Silva and Karem Sakallah's GRASP (1996) and was sped up by Chaff (2001). In 2016 a SAT solver settled the Boolean Pythagorean triples problem with a 200-terabyte proof.
Usage note
NP-completeness is a worst-case statement: real-world instances often have structure that CDCL exploits. Randomly generated 3-SAT formulas are empirically hardest near about 4.27 clauses per variable.
Related
- propositional logicpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true.
- NP-completeNP-complete, adj.: Describes problems, such as solving giant Sudokus, where a proposed answer is quick to check but no known method finds one quickly; a fast method for any one of them could be turned into one for all.
- satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.
- constraint satisfaction problemconstraint satisfaction problem, n.: A problem in which each item must be given a value so that every rule is obeyed, like filling in a Sudoku, coloring a map so no neighbors match, or building a timetable without clashes.
- resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.
- answer set programminganswer set programming, n.: A way to solve hard puzzles and scheduling problems by describing in logical rules what a valid solution looks like; a solver then finds the arrangements that fit those rules.
- combinatorial explosioncombinatorial explosion, n.: The way the number of possible combinations — moves, routes, schedules — grows so quickly as a problem gets bigger that checking them all becomes impossible, even for the fastest computers.
Sources
- Cook, S. A. (1971). The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd ACM Symposium on Theory of Computing, 151–158.
- Davis, M., Logemann, G. & Loveland, D. (1962). A Machine Program for Theorem-Proving. Communications of the ACM 5(7), 394–397.
- Heule, M. J. H., Kullmann, O. & Marek, V. W. (2016). Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT 2016, LNCS 9710.
Mentioned in
modelmodel, n.: A simplified working version of something. In AI it usually means the trained program, a big set of learned numbers, that takes an input and produces an answer, prediction or piece of content., symbolic AIsymbolic AI, n.: An approach to AI that writes knowledge down as human-readable symbols and rules, such as 'every bird has wings', and reasons by manipulating them step by step instead of learning patterns from data., automated planningautomated planning, n.: The branch of AI that works out a sequence of actions to reach a goal, such as the steps a robot must take to assemble a part, from descriptions of what each action needs and what it changes., combinatorial explosioncombinatorial explosion, n.: The way the number of possible combinations — moves, routes, schedules — grows so quickly as a problem gets bigger that checking them all becomes impossible, even for the fastest computers., constraint satisfaction problemconstraint satisfaction problem, n.: A problem in which each item must be given a value so that every rule is obeyed, like filling in a Sudoku, coloring a map so no neighbors match, or building a timetable without clashes., good old-fashioned AIgood old-fashioned AI, n.: A nickname for the classic style of AI, dominant from the 1950s to the 1980s, that tried to make computers intelligent by writing knowledge and rules down by hand., NP-completeNP-complete, adj.: Describes problems, such as solving giant Sudokus, where a proposed answer is quick to check but no known method finds one quickly; a fast method for any one of them could be turned into one for all., propositional logicpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true., answer set programminganswer set programming, n.: A way to solve hard puzzles and scheduling problems by describing in logical rules what a valid solution looks like; a solver then finds the arrangements that fit those rules., Horn clauseHorn clause, n.: A simple, restricted form of logical rule ('if these conditions all hold, then this one conclusion holds') that computers can reason with very efficiently., integer programminginteger programming, n.: Finding the best plan when some decisions must be whole numbers or yes-or-no choices — you cannot open half a warehouse or send 2.7 trucks. That small change makes the best plan far harder to find., local searchlocal search, n.: A family of problem-solving methods that start with some complete answer, however poor, and keep improving it by small changes, instead of building an answer piece by piece from scratch., resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known., satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.