Inlogic andcomputer science, theBoolean satisfiability problem (sometimes calledpropositional satisfiability problem and abbreviatedSATISFIABILITY,SAT orB-SAT) asks whether there exists aninterpretation thatsatisfies a givenBooleanformula. In other words, it asks whether the formula's variables can be consistently replaced by the values TRUE or FALSE to make the formula evaluate to TRUE. If this is the case, the formula is calledsatisfiable, elseunsatisfiable. For example, the formula "a AND NOTb" is satisfiable because one can find the valuesa = TRUE andb = FALSE, which make (a AND NOTb) = TRUE. In contrast, "a AND NOTa" is unsatisfiable.
SAT is the first problem that was proven to beNP-complete—this is theCook–Levin theorem. This means that all problems in the complexity classNP, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem (where "efficiently" means "deterministically inpolynomial time"). Although such an algorithm is generally believed not to exist, this belief has not been proven or disproven mathematically. Resolving the question of whether SAT has apolynomial-time algorithm would settle theP versus NP problem - one of the most important open problems in the theory of computing.[1][2]
Nevertheless, as of 2007, heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols,[3] which is sufficient for many practical SAT problems occurring inartificial intelligence,circuit design,[4] andautomatic theorem proving.
Apropositional logic formula, also calledBoolean expression, is built fromvariables, operators AND (conjunction, also denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬), and parentheses. A formula is said to besatisfiable if it can be made TRUE by assigning appropriatelogical values (i.e. TRUE, FALSE) to its variables. TheBoolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. Thisdecision problem is of central importance in many areas ofcomputer science, includingtheoretical computer science,complexity theory,[5][6]algorithmics,cryptography[7][8] andartificial intelligence.[9][additional citation(s) needed]
Aliteral is either a variable (in which case it is called apositive literal) or the negation of a variable (called anegative literal). Aclause is a disjunction of literals (or a single literal). A clause is called aHorn clause if it contains at most one positive literal. A formula is inconjunctive normal form (CNF) if it is a conjunction of clauses (or a single clause).
For example,x1 is a positive literal,¬x2 is a negative literal, andx1 ∨ ¬x2 is a clause. The formula(x1 ∨ ¬x2) ∧ (¬x1 ∨x2 ∨x3) ∧ ¬x1 is in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable, by choosingx1 = FALSE,x2 = FALSE, andx3 arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨x3) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨x3) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formulaa ∧ ¬a, consisting of two clauses of one literal, is unsatisfiable, since fora=TRUE ora=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e., FALSE) or FALSE ∧ ¬FALSE (i.e., again FALSE), respectively.
For some versions of the SAT problem, it is useful to define the notion of ageneralized conjunctive normal form formula, viz. as a conjunction of arbitrarily manygeneralized clauses, the latter being of the formR(l1,...,ln) for someBoolean functionR and (ordinary) literalsli. Different sets of allowed Boolean functions lead to different problem versions. As an example,R(¬x,a,b) is a generalized clause, andR(¬x,a,b) ∧R(b,y,c) ∧R(c,d,¬z) is a generalized conjunctive normal form. This formula is usedbelow, withR being the ternary operator that is TRUE just when exactly one of its arguments is.
Using the laws ofBoolean algebra, every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer. For example, transforming the formula (x1∧y1) ∨ (x2∧y2) ∨ ... ∨ (xn∧yn) into conjunctive normal form yields
while the former is a disjunction ofn conjunctions of 2 variables, the latter consists of 2n clauses ofn variables.
However, with use of theTseytin transformation, we may find an equisatisfiable conjunctive normal form formula with length linear in the size of the original propositional logic formula.
SAT was the first problem known to beNP-complete, as proved byStephen Cook at theUniversity of Toronto in 1971[10] and independently byLeonid Levin at theRussian Academy of Sciences in 1973.[11] Until that time, the concept of an NP-complete problem did not even exist. The proof shows how every decision problem in thecomplexity classNP can bereduced to the SAT problem for CNF[a] formulas, sometimes calledCNFSAT. A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, deciding whether a givengraph has a3-coloring is another problem in NP; if a graph has 17 valid 3-colorings, then the SAT formula produced by the Cook–Levin reduction will have 17 satisfying assignments.
NP-completeness only refers to the run-time of the worst case instances. Many of the instances that occur in practical applications can be solved much more quickly. See§Algorithms for solving SAT below.
Like the satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called3-SAT,3CNFSAT, or3-satisfiability. To reduce the unrestricted SAT problem to 3-SAT, transform each clausel1 ∨ ⋯ ∨ln to a conjunction ofn - 2 clauses
wherex2, ⋯ , xn−2 arefresh variables not occurring elsewhere. Although the two formulas are notlogically equivalent, they areequisatisfiable. The formula resulting from transforming all clauses is at most 3 times as long as its original; that is, the length growth is polynomial.[12]
3-SAT is one ofKarp's 21 NP-complete problems, and it is used as a starting point for proving that other problems are alsoNP-hard.[b] This is done bypolynomial-time reduction from 3-SAT to the other problem. An example of a problem where this method has been used is theclique problem: given a CNF formula consisting ofc clauses, the correspondinggraph consists of a vertex for each literal, and an edge between each two non-contradicting[c] literals from different clauses; see the picture. The graph has ac-clique if and only if the formula is satisfiable.[13]
There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)n wheren is the number of variables in the 3-SAT proposition, and succeeds with high probability to correctly decide 3-SAT.[14]
Theexponential time hypothesis asserts that no algorithm can solve 3-SAT (or indeedk-SAT for anyk > 2) inexp(o(n)) time (that is, fundamentally faster than exponential inn).
Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3-SAT formulas, depending on their size parameters. Difficulty is measured in number recursive calls made by aDPLL algorithm. They identified a phase transition region from almost-certainly-satisfiable to almost-certainly-unsatisfiable formulas at the clauses-to-variables ratio at about 4.26.[15]
3-satisfiability can be generalized tok-satisfiability (k-SAT, alsok-CNF-SAT), when formulas in CNF are considered with each clause containing up tok literals.[citation needed] However, since for anyk ≥ 3, this problem can neither be easier than 3-SAT nor harder than SAT, and the latter two are NP-complete, so must be k-SAT.
Some authors restrict k-SAT to CNF formulas withexactly k literals.[citation needed] This does not lead to a different complexity class either, as each clausel1 ∨ ⋯ ∨lj withj <k literals can be padded with fixed dummy variables tol1 ∨ ⋯ ∨lj ∨dj+1 ∨ ⋯ ∨dk. After padding all clauses, 2k–1 extra clauses[d] must be appended to ensure that onlyd1 = ⋯ =dk = FALSE can lead to a satisfying assignment. Sincek does not depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whetherduplicate literals are allowed in clauses, as in¬x ∨ ¬y ∨ ¬y.
Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above, the general SAT problem reduces to 3-SAT, the problem of determining satisfiability for formulas in this form.
A 3-SAT formula isLinear SAT (LSAT) if each clause (viewed as a set of literals) intersects at most one other clause, and, moreover, if two clauses intersect, then they have exactly one literal in common. An LSAT formula can be depicted as a set of disjoint semi-closed intervals on a line. Deciding whether an LSAT formula is satisfiable is NP-complete.[16]
SAT is easier if the number of literals in a clause is limited to at most 2, in which case the problem is called2-SAT. This problem can be solved in polynomial time, and in fact iscomplete for the complexity classNL. If additionally all OR operations in literals are changed toXOR operations, then the result is calledexclusive-or 2-satisfiability, which is a problem complete for the complexity classSL =L.
The problem of deciding the satisfiability of a given conjunction ofHorn clauses is calledHorn-satisfiability, orHORN-SAT. It can be solved in polynomial time by a single step of theunit propagation algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Horn-satisfiability isP-complete. It can be seen asP's version of the Boolean satisfiability problem. Also, deciding the truth of quantified Horn formulas can be done in polynomial time.[17]
Horn clauses are of interest because they are able to expressimplication of one variable from a set of other variables. Indeed, one such clause ¬x1 ∨ ... ∨ ¬xn ∨y can be rewritten asx1 ∧ ... ∧xn →y; that is, ifx1,...,xn are all TRUE, theny must be TRUE as well.
A generalization of the class of Horn formulas is that of renameable-Horn formulae, which is the set of formulas that can be placed in Horn form by replacing some variables with their respective negation. For example, (x1 ∨ ¬x2) ∧ (¬x1 ∨x2 ∨x3) ∧ ¬x1 is not a Horn formula, but can be renamed to the Horn formula (x1 ∨ ¬x2) ∧ (¬x1 ∨x2 ∨ ¬y3) ∧ ¬x1 by introducingy3 as negation ofx3. In contrast, no renaming of (x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨x2 ∨x3) ∧ ¬x1 leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.
SAT is trivial if the formulas are restricted to those indisjunctive normal form, that is, they are a disjunction of conjunctions of literals. Such a formula is indeed satisfiable if and only if at least one of its conjunctions is satisfiable, and a conjunction is satisfiable if and only if it does not contain bothx and NOTx for some variablex. This can be checked in linear time. Furthermore, if they are restricted to being infull disjunctive normal form, in which every variable appears exactly once in every conjunction, they can be checked in constant time (each conjunction represents one satisfying assignment). But it can take exponential time and space to convert a general SAT problem to disjunctive normal form; to obtain an example, exchange "∧" and "∨" in theabove exponential blow-up example for conjunctive normal forms.
Another NP-complete variant of the 3-satisfiability problem is theone-in-three 3-SAT (also known variously as1-in-3-SAT andexactly-1 3-SAT). Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists a truth assignment to the variables so that each clause hasexactly one TRUE literal (and thus exactly two FALSE literals).
Another variant is thenot-all-equal 3-satisfiability problem (also calledNAE3SAT). Given a conjunctive normal form with three literals per clause, the problem is to determine if an assignment to the variables exists such that in no clause all three literals have the same truth value. This problem is NP-complete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem.[18]
Another special case is the class of problems where each clause contains XOR (i.e.exclusive or) rather than (plain) OR operators. This is inP, since an XOR-SAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time byGaussian elimination.[19]
The restrictions above (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bound the considered formulae to be conjunctions of subformulas; each restriction states a specific form for all subformulas: for example, only binary clauses can be subformulas in 2CNF.
Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulas, the corresponding satisfiability problem is in P or NP-complete. The membership in P of the satisfiability of 2CNF, Horn, and XOR-SAT formulae are special cases of this theorem.[18]
The following table summarizes some common variants of SAT.
| Name | Code | 3SAT problem? | Restrictions | Requirements | Class |
|---|---|---|---|---|---|
| 3-satisfiability | 3SAT | Yes | Each clause contains 3 literals. | At least one literal must be true. | NP-c |
| 2-satisfiability | 2SAT | Yes | Each clause contains 2 literals. | At least one literal must be true. | NL-c |
| Exactly-1 3-SAT | 1-in-3-SAT | No | Each clause contains 3 literals. | Exactly one literal must be true. | NP-c |
| Exactly-1 Positive 3-SAT | 1-in-3-SAT+ | No | Each clause contains 3 positive literals. | Exactly one literal must be true. | NP-c |
| Not-all-equal 3-satisfiability | NAE3SAT | No | Each clause contains 3 literals. | Either one or two literals must be true. | NP-c |
| Not-all-equal positive 3-SAT | NAE3SAT+ | No | Each clause contains 3 positive literals. | Either one or two literals must be true. | NP-c |
| Planar SAT | PL-SAT | Yes | The incidence graph (clause-variable graph) isplanar. | At least one literal must be true. | NP-c |
| Linear SAT | LSAT | Yes | Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal. | At least one literal must be true. | NP-c |
| Horn satisfiability | HORN-SAT | Yes | Horn clauses (at most one positive literal). | At least one literal must be true. | P-c |
| Xor satisfiability | XOR-SAT | No | Each clause contains XOR operations rather than OR. | The XOR of all literals must be true. | P |
An extension that has gained significant popularity since 2003 issatisfiability modulo theories (SMT) that can enrich CNF formulas with linear constraints, arrays, all-different constraints,uninterpreted functions,[20] etc. Such extensions typically remain NP-complete, but very efficient solvers are now available that can handle many such kinds of constraints.
The satisfiability problem becomes more difficult if both "for all" (∀) and "there exists" (∃)quantifiers are allowed to bind the Boolean variables. An example of such an expression would be∀x ∀y ∃z (x ∨y ∨z) ∧ (¬x ∨ ¬y ∨ ¬z); it is valid, since for all values ofx andy, an appropriate value ofz can be found, viz.z=TRUE if bothx andy are FALSE, andz=FALSE else. SAT itself (tacitly) uses only ∃ quantifiers. If only ∀ quantifiers are allowed instead, the so-calledtautology problem is obtained, which isco-NP-complete. If any number of both quantifiers are allowed, the problem is called thequantified Boolean formula problem (QBF), which can be shown to bePSPACE-complete. It is widely believed that PSPACE-complete problems are strictly harder than any problem in NP, although this has not yet been proved.
Ordinary SAT asks if there is at least one variable assignment that makes the formula true. A variety of variants deal with the number of such assignments:
Other generalizations include satisfiability forfirst- andsecond-order logic,constraint satisfaction problems,0-1 integer programming.
While SAT is adecision problem, thesearch problem of finding a satisfying assignment reduces to SAT. That is, each algorithm which correctly answers whether an instance of SAT is solvable can be used to find a satisfying assignment. First, the question is asked on the given formula Φ. If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on the partly instantiated formula Φ{x1=TRUE}, that is, Φ with the first variablex1 replaced by TRUE, and simplified accordingly. If the answer is "yes", thenx1=TRUE, otherwisex1=FALSE. Values of other variables can be found subsequently in the same way. In total,n+1 runs of the algorithm are required, wheren is the number of distinct variables in Φ.
This property is used in several theorems in complexity theory:
Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).[3] Examples of such problems inelectronic design automation (EDA) includeformal equivalence checking,model checking,formal verification ofpipelined microprocessors,[20]automatic test pattern generation,routing ofFPGAs,[27]planning, andscheduling problems, and so on. A SAT-solving engine is also considered to be an essential component in theelectronic design automation toolbox.
Major techniques used by modern SAT solvers include theDavis–Putnam–Logemann–Loveland algorithm (or DPLL),conflict-driven clause learning (CDCL), andstochasticlocal search algorithms such asWalkSAT. Almost all SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution. Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. Recent attempts have been made to learn an instance's satisfiability using deep learning techniques.[28]
SAT solvers are developed and compared in SAT-solving contests.[29] Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, andoperations research, among others.
Theoretical algorithms with increasingly better worst-case runtime guarantees have been given in the last decades, including an algorithm for clause sets of length (total literal count),[30][31]an algorithm for sets of clauses,[32][33] and an algorithm for 3-SAT with variables.[34] Here, the notation "" means "up to a polynomial factor", i.e.. Earlier runtime guarantees are shown in the diagram.
modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables.
(by date of publication)
| Major fields |
| ||||
|---|---|---|---|---|---|
| Foundations | |||||
| Lists |
| ||||
