In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or BSAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.
SAT is the first problem that was proven to be NPcomplete; see Cook–Levin theorem. This means that all problems in the complexity class NP, 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, and it is generally believed that no such algorithm exists; yet this belief has not been proven mathematically, and resolving the question of whether SAT has a polynomialtime algorithm is equivalent to the P versus NP problem, which is a famous open problem in the theory of computing.
Nevertheless, as of 2007, heuristic SATalgorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols,^{[1]} which is sufficient for many practical SAT problems from, e.g., artificial intelligence, circuit design,^{[2]} and automatic theorem proving.
Basic definitions and terminologyEdit
A propositional logic formula, also called Boolean expression, is built from variables, operators AND (conjunction, also denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬), and parentheses. A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables. The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. This decision problem is of central importance in many areas of computer science, including theoretical computer science, complexity theory,^{[3]}^{[4]} algorithmics, cryptography^{[5]}^{[6]} and artificial intelligence.^{[7]}^{[additional citation(s) needed]}
There are several special cases of the Boolean satisfiability problem in which the formulas are required to have a particular structure. A literal is either a variable, called positive literal, or the negation of a variable, called negative literal. A clause is a disjunction of literals (or a single literal). A clause is called a Horn clause if it contains at most one positive literal. A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses (or a single clause). For example, x_{1} is a positive literal, ¬x_{2} is a negative literal, x_{1} ∨ ¬x_{2} is a clause. The formula (x_{1} ∨ ¬x_{2}) ∧ (¬x_{1} ∨ x_{2} ∨ x_{3}) ∧ ¬x_{1} is in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable, by choosing x_{1} = FALSE, x_{2} = FALSE, and x_{3} arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x_{3}) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x_{3}) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula a ∧ ¬a, consisting of two clauses of one literal, is unsatisfiable, since for a=TRUE or a=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 a generalized conjunctive normal form formula, viz. as a conjunction of arbitrarily many generalized clauses, the latter being of the form R(l_{1},...,l_{n}) for some boolean operator R and (ordinary) literals l_{i}. Different sets of allowed boolean operators lead to different problem versions. As an example, R(¬x,a,b) is a generalized clause, and R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z) is a generalized conjunctive normal form. This formula is used below, with R being the ternary operator that is TRUE just when exactly one of its arguments is.
Using the laws of Boolean 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 (x_{1}∧y_{1}) ∨ (x_{2}∧y_{2}) ∨ ... ∨ (x_{n}∧y_{n}) into conjunctive normal form yields
 (x_{1} ∨ x_{2} ∨ … ∨ x_{n}) ∧
 (y_{1} ∨ x_{2} ∨ … ∨ x_{n}) ∧
 (x_{1} ∨ y_{2} ∨ … ∨ x_{n}) ∧
 (y_{1} ∨ y_{2} ∨ … ∨ x_{n}) ∧ ... ∧
 (x_{1} ∨ x_{2} ∨ … ∨ y_{n}) ∧
 (y_{1} ∨ x_{2} ∨ … ∨ y_{n}) ∧
 (x_{1} ∨ y_{2} ∨ … ∨ y_{n}) ∧
 (y_{1} ∨ y_{2} ∨ … ∨ y_{n});
while the former is a disjunction of n conjunctions of 2 variables, the latter consists of 2^{n} clauses of n variables.
Complexity and restricted versionsEdit
Unrestricted satisfiability (SAT)Edit
SAT was the first known NPcomplete problem, as proved by Stephen Cook at the University of Toronto in 1971^{[8]} and independently by Leonid Levin at the National Academy of Sciences in 1973.^{[9]} Until that time, the concept of an NPcomplete problem did not even exist. The proof shows how every decision problem in the complexity class NP can be reduced to the SAT problem for CNF^{[note 1]} formulas, sometimes called CNFSAT. A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, deciding whether a given graph has a 3coloring is another problem in NP; if a graph has 17 valid 3colorings, the SAT formula produced by the Cook–Levin reduction will have 17 satisfying assignments.
NPcompleteness only refers to the runtime 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.
SAT is trivial if the formulas are restricted to those in disjunctive normal form, that is, they are 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 both x and NOT x for some variable x. This can be checked in linear time. Furthermore, if they are restricted to being in full 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; for an example exchange "∧" and "∨" in the above exponential blowup example for conjunctive normal forms.
3satisfiabilityEdit
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 NPcomplete also; this problem is called 3SAT, 3CNFSAT, or 3satisfiability. To reduce the unrestricted SAT problem to 3SAT, transform each clause l_{1} ∨ ⋯ ∨ l_{n} to a conjunction of n − 2 clauses
 (l_{1} ∨ l_{2} ∨ x_{2}) ∧
 (¬x_{2} ∨ l_{3} ∨ x_{3}) ∧
 (¬x_{3} ∨ l_{4} ∨ x_{4}) ∧ ⋯ ∧
 (¬x_{n − 3} ∨ l_{n − 2} ∨ x_{n − 2}) ∧
 (¬x_{n − 2} ∨ l_{n − 1} ∨ l_{n})
where x_{2}, ⋯ , x_{n − 2} are fresh variables not occurring elsewhere. Although the two formulas are not logically equivalent, they are equisatisfiable. The formula resulting from transforming all clauses is at most 3 times as long as its original, i.e. the length growth is polynomial.^{[10]}
3SAT is one of Karp's 21 NPcomplete problems, and it is used as a starting point for proving that other problems are also NPhard.^{[note 2]} This is done by polynomialtime reduction from 3SAT to the other problem. An example of a problem where this method has been used is the clique problem: given a CNF formula consisting of c clauses, the corresponding graph consists of a vertex for each literal, and an edge between each two noncontradicting^{[note 3]} literals from different clauses, cf. picture. The graph has a cclique if and only if the formula is satisfiable.^{[11]}
There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)^{n} where n is the number of variables in the 3SAT proposition, and succeeds with high probability to correctly decide 3SAT.^{[12]}
The exponential time hypothesis asserts that no algorithm can solve 3SAT (or indeed kSAT for any k > 2) in exp(o(n)) time (i.e., fundamentally faster than exponential in n).
Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3SAT formulas, depending on their size parameters. Difficulty is measured in number recursive calls made by a DPLL algorithm.^{[13]}
3satisfiability can be generalized to ksatisfiability (kSAT, also kCNFSAT), when formulas in CNF are considered with each clause containing up to k literals.^{[citation needed]} However, since for any k ≥ 3, this problem can neither be easier than 3SAT nor harder than SAT, and the latter two are NPcomplete, so must be kSAT.
Some authors restrict kSAT to CNF formulas with exactly k literals.^{[citation needed]} This doesn't lead to a different complexity class either, as each clause l_{1} ∨ ⋯ ∨ l_{j} with j < k literals can be padded with fixed dummy variables to l_{1} ∨ ⋯ ∨ l_{j} ∨ d_{j+1} ∨ ⋯ ∨ d_{k}. After padding all clauses, 2^{k}1 extra clauses^{[note 4]} have to be appended to ensure that only d_{1} = ⋯ = d_{k}=FALSE can lead to a satisfying assignment. Since k doesn't depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whether duplicate literals are allowed in clauses, as in ¬x ∨ ¬y ∨ ¬y.
Exactly1 3satisfiabilityEdit
A variant of the 3satisfiability problem is the oneinthree 3SAT (also known variously as 1in3SAT and exactly1 3SAT). 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 has exactly one TRUE literal (and thus exactly two FALSE literals). In contrast, ordinary 3SAT requires that every clause has at least one TRUE literal. Formally, a oneinthree 3SAT problem is given as a generalized conjunctive normal form with all generalized clauses using a ternary operator R that is TRUE just if exactly one of its arguments is. When all literals of a oneinthree 3SAT formula are positive, the satisfiability problem is called oneinthree positive 3SAT.
Oneinthree 3SAT, together with its positive case, is listed as NPcomplete problem "LO4" in the standard reference, Computers and Intractability: A Guide to the Theory of NPCompleteness by Michael R. Garey and David S. Johnson. Oneinthree 3SAT was proved to be NPcomplete by Thomas Jerome Schaefer as a special case of Schaefer's dichotomy theorem, which asserts that any problem generalizing Boolean satisfiability in a certain way is either in the class P or is NPcomplete.^{[14]}
Schaefer gives a construction allowing an easy polynomialtime reduction from 3SAT to oneinthree 3SAT. Let "(x or y or z)" be a clause in a 3CNF formula. Add six fresh boolean variables a, b, c, d, e, and f, to be used to simulate this clause and no other. Then the formula R(x,a,d) ∧ R(y,b,d) ∧ R(a,b,e) ∧ R(c,d,f) ∧ R(z,c,FALSE) is satisfiable by some setting of the fresh variables if and only if at least one of x, y, or z is TRUE, see picture (left). Thus any 3SAT instance with m clauses and n variables may be converted into an equisatisfiable oneinthree 3SAT instance with 5m clauses and n+6m variables.^{[15]} Another reduction involves only four fresh variables and three clauses: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), see picture (right).
Notallequal 3satisfiabilityEdit
Another variant is the notallequal 3satisfiability problem (also called NAE3SAT). 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 NPcomplete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem.^{[14]}
Linear SATEdit
A 3SAT formula is Linear 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 semiclosed intervals on a line. Deciding whether an LSAT formula is satisfiable or not is NPcomplete.^{[16]}
2satisfiabilityEdit
SAT is easier if the number of literals in a clause is limited to at most 2, in which case the problem is called 2SAT. This problem can be solved in polynomial time, and in fact is complete for the complexity class NL. If additionally all OR operations in literals are changed to XOR operations, the result is called exclusiveor 2satisfiability, which is a problem complete for the complexity class SL = L.
HornsatisfiabilityEdit
The problem of deciding the satisfiability of a given conjunction of Horn clauses is called Hornsatisfiability, or HORNSAT. It can be solved in polynomial time by a single step of the Unit propagation algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Hornsatisfiability is Pcomplete. It can be seen as P'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 express implication of one variable from a set of other variables. Indeed, one such clause ¬x_{1} ∨ ... ∨ ¬x_{n} ∨ y can be rewritten as x_{1} ∧ ... ∧ x_{n} → y, that is, if x_{1},...,x_{n} are all TRUE, then y needs to be TRUE as well.
A generalization of the class of Horn formulae is that of renameableHorn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. For example, (x_{1} ∨ ¬x_{2}) ∧ (¬x_{1} ∨ x_{2} ∨ x_{3}) ∧ ¬x_{1} is not a Horn formula, but can be renamed to the Horn formula (x_{1} ∨ ¬x_{2}) ∧ (¬x_{1} ∨ x_{2} ∨ ¬y_{3}) ∧ ¬x_{1} by introducing y_{3} as negation of x_{3}. In contrast, no renaming of (x_{1} ∨ ¬x_{2} ∨ ¬x_{3}) ∧ (¬x_{1} ∨ x_{2} ∨ x_{3}) ∧ ¬x_{1} 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.
XORsatisfiabilityEdit
Solving an XORSAT example by Gaussian elimination  

 
 
 
 
 
 

Another special case is the class of problems where each clause contains XOR (i.e. exclusive or) rather than (plain) OR operators.^{[note 5]} This is in P, since an XORSAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time by Gaussian elimination;^{[18]} see the box for an example. This recast is based on the kinship between Boolean algebras and Boolean rings, and the fact that arithmetic modulo two forms a finite field. Since a XOR b XOR c evaluates to TRUE if and only if exactly 1 or 3 members of {a,b,c} are TRUE, each solution of the 1in3SAT problem for a given CNF formula is also a solution of the XOR3SAT problem, and in turn each solution of XOR3SAT is a solution of 3SAT, cf. picture. As a consequence, for each CNF formula, it is possible to solve the XOR3SAT problem defined by the formula, and based on the result infer either that the 3SAT problem is solvable or that the 1in3SAT problem is unsolvable.
Provided that the complexity classes P and NP are not equal, neither 2, nor Horn, nor XORsatisfiability is NPcomplete, unlike SAT.
Schaefer's dichotomy theoremEdit
The restrictions above (CNF, 2CNF, 3CNF, Horn, XORSAT) bound the considered formulae to be conjunctions of subformulae; each restriction states a specific form for all subformulae: for example, only binary clauses can be subformulae in 2CNF.
Schaefer's dichotomy theorem states that, for any restriction to Boolean operators that can be used to form these subformulae, the corresponding satisfiability problem is in P or NPcomplete. The membership in P of the satisfiability of 2CNF, Horn, and XORSAT formulae are special cases of this theorem.^{[14]}
The following table summarizes some common variants of SAT.
Code  Name  Restrictions  Requirements  Class 

3SAT  3satisfiability  Each clause contains 3 literals.  At least one literal must be true.  NPC 
2SAT  2satisfiability  Each clause contains 2 literals.  At least one literal must be true.  P 
1in3SAT  Exactly1 3SAT  Each clause contains 3 literals.  Exactly one literal must be true.  NPC 
1in3SAT+  Exactly1 Positive 3SAT  Each clause contains 3 positive literals.  Exactly one literal must be true.  NPC 
NAE3SAT  Notallequal 3satisfiability  Each clause contains 3 literals.  Either one or two literals must be true.  NPC 
NAE3SAT+  Notallequal positive 3SAT  Each clause contains 3 positive literals.  Either one or two literals must be true.  NPC 
PLSAT  Planar SAT  The incidence graph (clausevariable graph) is planar.  At least one literal must be true.  NPC 
L3SAT  Linear 3SAT  Each clause intersects at most one other clause, and the intersection is exactly one literal.  At least one literal must be true.  NPC 
HORNSAT  Horn satisfiability  Horn clauses (at most one positive literal).  At least one literal must be true.  P 
XORSAT  Xor satisfiability  Each clause contains XOR operations rather than OR.  The XOR of all literals must be true.  P 
Extensions of SATEdit
An extension that has gained significant popularity since 2003 is satisfiability modulo theories (SMT) that can enrich CNF formulas with linear constraints, arrays, alldifferent constraints, uninterpreted functions,^{[19]} etc. Such extensions typically remain NPcomplete, 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 of x and y, an appropriate value of z can be found, viz. z=TRUE if both x and y are FALSE, and z=FALSE else. SAT itself (tacitly) uses only ∃ quantifiers. If only ∀ quantifiers are allowed instead, the socalled tautology problem is obtained, which is coNPcomplete. If both quantifiers are allowed, the problem is called the quantified Boolean formula problem (QBF), which can be shown to be PSPACEcomplete. It is widely believed that PSPACEcomplete problems are strictly harder than any problem in NP, although this has not yet been proved. Using highly parallel P systems, QBFSAT problems can be solved in linear time.^{[20]}
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:
 MAJSAT asks if the majority of all assignments make the formula TRUE. It is known to be complete for PP, a probabilistic class.
 #SAT, the problem of counting how many variable assignments satisfy a formula, is a counting problem, not a decision problem, and is #Pcomplete.
 UNIQUE SAT^{[21]} is the problem of determining whether a formula has exactly one assignment. It is complete for US,^{[22]} the complexity class describing problems solvable by a nondeterministic polynomial time Turing machine that accepts when there is exactly one nondeterministic accepting path and rejects otherwise.
 UNAMBIGUOUSSAT is the name given to the satisfiability problem when the input is restricted to formulas having at most one satisfying assignment. The problem is also called USAT.^{[23]} A solving algorithm for UNAMBIGUOUSSAT is allowed to exhibit any behavior, including endless looping, on a formula having several satisfying assignments. Although this problem seems easier, Valiant and Vazirani have shown^{[24]} that if there is a practical (i.e. randomized polynomialtime) algorithm to solve it, then all problems in NP can be solved just as easily.
 MAXSAT, the maximum satisfiability problem, is an FNP generalization of SAT. It asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient approximation algorithms, but is NPhard to solve exactly. Worse still, it is APXcomplete, meaning there is no polynomialtime approximation scheme (PTAS) for this problem unless P=NP.
 WMSAT is the problem of finding an assignment of minimum weight that satisfy a monotone Boolean formula (i.e. a formula without any negation). Weights of propositional variables are given in the input of the problem. The weight of an assignment is the sum of weights of true variables. That problem is NPcomplete (see Th. 1 of ^{[25]}).
Other generalizations include satisfiability for first and secondorder logic, constraint satisfaction problems, 01 integer programming.
SelfreducibilityEdit
The SAT problem is selfreducible, that is, each algorithm which correctly answers if 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 Φ{x_{1}=TRUE}, i.e. Φ with the first variable x_{1} replaced by TRUE, and simplified accordingly. If the answer is "yes", then x_{1}=TRUE, otherwise x_{1}=FALSE. Values of other variables can be found subsequently in the same way. In total, n+1 runs of the algorithm are required, where n is the number of distinct variables in Φ.
This property of selfreducibility is used in several theorems in complexity theory:
Algorithms for solving SATEdit
Since the SAT problem is NPcomplete, only algorithms with exponential worstcase 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 our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).^{[1]} Examples of such problems in electronic design automation (EDA) include formal equivalence checking, model checking, formal verification of pipelined microprocessors,^{[19]} automatic test pattern generation, routing of FPGAs,^{[26]} planning, and scheduling problems, and so on. A SATsolving engine is now considered to be an essential component in the EDA toolbox.
A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 1960s (see references below) and is now commonly referred to as the Davis–Putnam–Logemann–Loveland algorithm ("DPLL" or "DLL").^{[27]}^{[28]} Many modern approaches to practical SAT solving are derived from the DPLL algorithm and share the same structure. Often they only improve the efficiency of certain classes of SAT problems such as instances that appear in industrial applications or randomly generated instances.^{[29]} Theoretically, exponential lower bounds have been proved for the DPLL family of algorithms.^{[citation needed]}
Algorithms that are not part of the DPLL family include stochastic local search algorithms. One example is WalkSAT. Stochastic methods try to find a satisfying interpretation but cannot deduce that a SAT instance is unsatisfiable, as opposed to complete algorithms, such as DPLL.^{[29]}
In contrast, randomized algorithms like the PPSZ algorithm by Paturi, Pudlak, Saks, and Zane set variables in a random order according to some heuristics, for example boundedwidth resolution. If the heuristic can't find the correct setting, the variable is assigned randomly. The PPSZ algorithm has a runtime^{[clarify]} of <math>O(1.308^n)</math> for 3SAT. This was the bestknown runtime for this problem until a recent improvement by Hansen, Kaplan, Zamir and Zwick that has a runtime of <math>O(1.307^n)</math> for 3SAT and currently the best known runtime for kSAT, for all values of k. In the setting with many satisfying assignments the randomized algorithm by Schöning has a better bound.^{[12]}^{[30]}^{[31]}
Modern SAT solvers (developed in the 2000s) come in two flavors: "conflictdriven" and "lookahead". Both approaches descend from DPLL.^{[29]} Conflictdriven solvers, such as conflictdriven clause learning (CDCL), augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, nonchronological backtracking (a.k.a. backjumping), as well as "twowatchedliterals" unit propagation, adaptive branching, and random restarts. These "extras" to the basic systematic search have been empirically shown to be essential for handling the large SAT instances that arise in electronic design automation (EDA).^{[32]} Well known implementations include Chaff^{[33]} and GRASP.^{[34]} Lookahead solvers have especially strengthened reductions (going beyond unitclause propagation) and the heuristics, and they are generally stronger than conflictdriven solvers on hard instances (while conflictdriven solvers can be much better on large instances which actually have an easy instance inside).
Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and operations research, among others. Powerful solvers are readily available as free and open source software. In particular, the conflictdriven MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code. A modern Parallel SAT solver is ManySAT.^{[35]} It can achieve super linear speedups on important classes of problems. An example for lookahead solvers is march_dl, which won a prize at the 2007 SAT competition.
Certain types of large random satisfiable instances of SAT can be solved by survey propagation (SP). Particularly in hardware design and verification applications, satisfiability and other logical properties of a given propositional formula are sometimes decided based on a representation of the formula as a binary decision diagram (BDD).
Almost all SAT solvers include timeouts, 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. All of these behaviors can be seen in the SAT solving contests.^{[36]}
Parallel SATsolvingEdit
Parallel SAT solvers come in three categories: portfolio, divideandconquer and parallel local search algorithms. With parallel portfolios, multiple different SAT solvers run concurrently. Each of them solves a copy of the SAT instance, whereas divideandconquer algorithms divide the problem between the processors. Different approaches exist to parallelize local search algorithms.
The International SAT Solver Competition has a parallel track reflecting recent advances in parallel SAT solving. In 2016,^{[37]} 2017^{[38]} and 2018,^{[39]} the benchmarks were run on a sharedmemory system with 24 processing cores, therefore solvers intended for distributed memory or manycore processors might have fallen short.
PortfoliosEdit
In general there is no SAT solver that performs better than all other solvers on all SAT problems. An algorithm might perform well for problem instances others struggle with, but will do worse with other instances. Furthermore, given a SAT instance, there is no reliable way to predict which algorithm will solve this instance particularly fast. These limitations motivate the parallel portfolio approach. A portfolio is a set of different algorithms or different configurations of the same algorithm. All solvers in a parallel portfolio run on different processors to solve of the same problem. If one solver terminates, the portfolio solver reports the problem to be satisfiable or unsatisfiable according to this one solver. All other solvers are terminated. Diversifying portfolios by including a variety of solvers, each performing well on a different set of problems, increases the robustness of the solver.^{[40]}
Many solvers internally use a random number generator. Diversifying their seeds is a simple way to diversify a portfolio. Other diversification strategies involve enabling, disabling or diversifying certain heuristics in the sequential solver.^{[41]}
One drawback of parallel portfolios is the amount of duplicate work. If clause learning is used in the sequential solvers, sharing learned clauses between parallel running solvers can reduce duplicate work and increase performance. Yet, even merely running a portfolio of the best solvers in parallel makes a competitive parallel solver. An example of such a solver is PPfolio.^{[42]}^{[43]} It was designed to find a lower bound for the performance a parallel SAT solver should be able to deliver. Despite the large amount of duplicate work due to lack of optimizations, it performed well on a shared memory machine. HordeSat^{[44]} is a parallel portfolio solver for large clusters of computing nodes. It uses differently configured instances of the same sequential solver at its core. Particularly for hard SAT instances HordeSat can produce linear speedups and therefore reduce runtime significantly.
In recent years parallel portfolio SAT solvers have dominated the parallel track of the International SAT Solver Competitions. Notable examples of such solvers include Plingeling and painlessmcomsps.^{[45]}
DivideandconquerEdit
In contrast to parallel portfolios, parallel divideandconquer tries to split the search space between the processing elements. Divideandconquer algorithms, such as the sequential DPLL, already apply the technique of splitting the search space, hence their extension towards a parallel algorithm is straight forward. However, due to techniques like unit propagation, following a division, the partial problems may differ significantly in complexity. Thus the DPLL algorithm typically does not process each part of the search space in the same amount of time, yielding a challenging load balancing problem.^{[40]}
Due to nonchronological backtracking, parallelization of conflictdriven clause learning is more difficult. One way to overcome this is the CubeandConquer paradigm.^{[46]} It suggests solving in two phases. In the "cube" phase the Problem is divided into many thousands, up to millions, of sections. This is done by a lookahead solver, that finds a set of partial configurations called "cubes". A cube can also be seen as a conjunction of a subset of variables of the original formula. In conjunction with the formula, each of the cubes forms a new formula. These formulas can be solved independently and concurrently by conflictdriven solvers. As the disjunction of these formulas is equivalent to the original formula, the problem is reported to be satisfiable, if one of the formulas is satisfiable. The lookahead solver is favorable for small but hard problems,^{[47]} so it is used to gradually divide the problem into multiple subproblems. These subproblems are easier but still large which is the ideal form for a conflictdriven solver. Furthermore lookahead solvers consider the entire problem whereas conflictdriven solvers make decisions based on information that is much more local. There are three heuristics involved in the cube phase. The variables in the cubes are chosen by the decision heuristic. The direction heuristic decides which variable assignment (true or false) to explore first. In satisfiable problem instances, choosing a satisfiable branch first is beneficial. The cutoff heuristic decides when to stop expanding a cube and instead forward it to a sequential conflictdriven solver. Preferably the cubes are similarly complex to solve.^{[46]}
Treengeling is an example for a parallel solver that applies the CubeandConquer paradigm. Since its introduction in 2012 it has had multiple successes at the International SAT Solver Competition. CubeandConquer was used to solve the Boolean Pythagorean triples problem.^{[48]}
Local searchEdit
One strategy towards a parallel local search algorithm for SAT solving is trying multiple variable flips concurrently on different processing units.^{[49]} Another is to apply the aforementioned portfolio approach, however clause sharing is not possible since local search solvers do not produce clauses. Alternatively, it is possible to share the configurations that are produced locally. These configurations can be used to guide the production of a new initial configuration when a local solver decides to restart its search.^{[50]}
See alsoEdit
 Unsatisfiable core
 Satisfiability modulo theories
 Counting SAT
 Planar SAT
 Karloff–Zwick algorithm
 Circuit satisfiability
NotesEdit
 ↑ The SAT problem for arbitrary formulas is NPcomplete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.
 ↑ i.e. at least as hard as every other problem in NP. A decision problem is NPcomplete if and only if it is in NP and is NPhard.
 ↑ i.e. such that one literal is not the negation of the other
 ↑ viz. all maxterms that can be built with d_{1},⋯,d_{k}, except d_{1}∨⋯∨d_{k}
 ↑ Formally, generalized conjunctive normal forms with a ternary boolean operator R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XORSAT can be reduced to XOR3SAT.
ReferencesEdit
 ↑ ^{1.0} ^{1.1} Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagation = Lazy Clause Generation", Principles and Practice of Constraint Programming – CP 2007, Lecture Notes in Computer Science, 4741, pp. 544–558, CiteSeerX 10.1.1.70.5471, doi:10.1007/9783540749707_39,
modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables
.  ↑ Hong, Ted; Li, Yanjing; Park, SungBoem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S.; Mitra, Subhasish (November 2010). "QED: Quick Error Detection tests for effective postsilicon validation". 2010 IEEE International Test Conference: 1–10. doi:10.1109/TEST.2010.5699215. ISBN 9781424472062. S2CID 7909084.
 ↑ Karp, Richard M. (1972). "Reducibility Among Combinatorial Problems" (PDF). In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. ISBN 0306307073. Here: p.86
 ↑ Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Reading/MA: AddisonWesley. ISBN 0201000296. Here: p.403
 ↑ Massacci, Fabio; Marraro, Laura (20000201). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165–203. doi:10.1023/A:1006326723002. ISSN 15730670.
 ↑ Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satisfiability Testing  SAT 2006. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 102–115. doi:10.1007/11814948_13. ISBN 9783540372073.
 ↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
 ↑ Cook, Stephen A. (1971). "The Complexity of TheoremProving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX 10.1.1.406.395. doi:10.1145/800157.805047. S2CID 7573663.
 ↑ Levin, Leonid (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). 9 (3): 115–116. (pdf) (in Russian), translated into English by Trakhtenbrot, B. A. (1984). "A survey of Russian approaches to perebor (bruteforce searches) algorithms". Annals of the History of Computing. 6 (4): 384–400. doi:10.1109/MAHC.1984.10036. S2CID 950581.
 ↑ ^{10.0} ^{10.1} Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. AddisonWesley.; here: Thm.10.4
 ↑ Aho, Hopcroft, Ullman^{[10]} (1974); Thm.10.5
 ↑ ^{12.0} ^{12.1} Schöning, Uwe (Oct 1999). "A Probabilistic Algorithm for kSAT and Constraint Satisfaction Problems" (PDF). Proc. 40th Ann. Symp. Foundations of Computer Science. pp. 410–414. doi:10.1109/SFFCS.1999.814612. ISBN 0769504094. S2CID 123177576.
 ↑ Bart Selman; David Mitchell; Hector Levesque (1996). "Generating Hard Satisfiability Problems". Artificial Intelligence. 81 (1–2): 17–29. CiteSeerX 10.1.1.37.7362. doi:10.1016/00043702(95)000453.
 ↑ ^{14.0} ^{14.1} ^{14.2} Schaefer, Thomas J. (1978). "The complexity of satisfiability problems" (PDF). Proceedings of the 10th Annual ACM Symposium on Theory of Computing. San Diego, California. pp. 216–226.
 ↑ (Schaefer, 1978), p.222, Lemma 3.5
 ↑ Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph S. B.; Simakov, Marina (20181211). "Selecting and covering colored points". Discrete Applied Mathematics. 250: 75–86. doi:10.1016/j.dam.2018.05.011. ISSN 0166218X.
 ↑ Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi:10.1006/inco.1995.1025.
 ↑ Moore, Cristopher; Mertens, Stephan (2011), The Nature of Computation, Oxford University Press, p. 366, ISBN 9780199233212.
 ↑ ^{19.0} ^{19.1} R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
 ↑ Alhazov, Artiom; MartínVide, Carlos; Pan, Linqiang (2003). "Solving a PSPACEComplete Problem by Recognizing P Systems with Restricted Active Membranes". Fundamenta Informaticae. 58: 67–77.
 ↑ Blass, Andreas; Gurevich, Yuri (19821001). "On the unique satisfiability problem". Information and Control. 55 (1): 80–88. doi:10.1016/S00199958(82)904399. ISSN 00199958.
 ↑ "Complexity Zoo:U  Complexity Zoo". complexityzoo.uwaterloo.ca. Retrieved 20191205.
 ↑ Kozen, Dexter C. (2006). "Supplementary Lecture F: Unique Satisfiability". Theory of Computation. Texts in Computer Science. London: SpringerVerlag. p. 180. ISBN 9781846282973.
 ↑ Valiant, L.; Vazirani, V. (1986). "NP is as easy as detecting unique solutions" (PDF). Theoretical Computer Science. 47: 85–93. doi:10.1016/03043975(86)901350.
 ↑ Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). Obana, Satoshi; Chida, Koji (eds.). "Simple Infeasibility Certificates for Attack Trees". Advances in Information and Computer Security. Lecture Notes in Computer Science. Springer International Publishing. 10418: 39–55. doi:10.1007/9783319642000_3. ISBN 9783319642000.
 ↑ GiJoon Nam; Sakallah, K. A.; Rutenbar, R. A. (2002). "A new FPGA detailed routing approach via searchbased Boolean satisfiability" (PDF). IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems. 21 (6): 674. doi:10.1109/TCAD.2002.1004311.
 ↑ Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201. doi:10.1145/321033.321034. S2CID 31888376.
 ↑ Davis, M.; Logemann, G.; Loveland, D. (1962). "A machine program for theoremproving" (PDF). Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
 ↑ ^{29.0} ^{29.1} ^{29.2} Zhang, Lintao; Malik, Sharad (2002), "The Quest for Efficient Boolean Satisfiability Solvers", Computer Aided Verification, Springer Berlin Heidelberg, pp. 17–36, doi:10.1007/3540456570_2, ISBN 9783540439974
 ↑ "An improved exponentialtime algorithm for kSAT", Paturi, Pudlak, Saks, Zani
 ↑ "Faster kSAT algorithms using biasedPPSZ", Hansen, Kaplan, Zamir, Zwick
 ↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
 ↑ Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S. (2001). "Chaff: Engineering an Efficient SAT Solver" (PDF). Proceedings of the 38th conference on Design automation (DAC). p. 530. doi:10.1145/378239.379017. ISBN 1581132972. S2CID 9292941.
 ↑ MarquesSilva, J. P.; Sakallah, K. A. (1999). "GRASP: a search algorithm for propositional satisfiability" (PDF). IEEE Transactions on Computers. 48 (5): 506. doi:10.1109/12.769433. Archived from the original (PDF) on 20161104. Retrieved 20150828.
 ↑ http://www.cril.univartois.fr/~jabbour/manysat.htm
 ↑ "The international SAT Competitions web page". Retrieved 20071115.
 ↑ "SAT Competition 2016". baldur.iti.kit.edu. Retrieved 20200213.
 ↑ "SAT Competition 2017". baldur.iti.kit.edu. Retrieved 20200213.
 ↑ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 20200213.
 ↑ ^{40.0} ^{40.1} Balyo, Tomáš; Sinz, Carsten (2018), "Parallel Satisfiability", Handbook of Parallel Constraint Reasoning, Springer International Publishing, pp. 3–29, doi:10.1007/9783319635163_1, ISBN 9783319635156
 ↑ Biere, Armin. "Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010" (PDF). SATRACE 2010.
 ↑ "ppfolio solver". www.cril.univartois.fr. Retrieved 20191229.
 ↑ "SAT 2011 Competition: 32 cores track: ranking of solvers". www.cril.univartois.fr. Retrieved 20200213.
 ↑ Balyo, Tomáš; Sanders, Peter; Sinz, Carsten (2015), "HordeSat: A Massively Parallel Portfolio SAT Solver", Lecture Notes in Computer Science, Springer International Publishing, pp. 156–172, arXiv:1505.03340, doi:10.1007/9783319243184_12, ISBN 9783319243177, S2CID 11507540
 ↑ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 20200213.
 ↑ ^{46.0} ^{46.1} Heule, Marijn J. H.; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", Hardware and Software: Verification and Testing, Springer Berlin Heidelberg, pp. 50–65, doi:10.1007/9783642341885_8, ISBN 9783642341878
 ↑ Heule, Marijn J. H.; van Maaren, Hans (2009). "LookAhead Based SAT Solvers" (PDF). Handbook of Satisfiability. IOS Press. pp. 155–184. ISBN 9781586039295.
 ↑ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016), "Solving and Verifying the Boolean Pythagorean Triples Problem via CubeandConquer", Theory and Applications of Satisfiability Testing – SAT 2016, Springer International Publishing, pp. 228–245, arXiv:1605.00723, doi:10.1007/9783319409702_15, ISBN 9783319409696, S2CID 7912943
 ↑ Roli, Andrea (2002), "Criticality and Parallelism in Structured SAT Instances", Principles and Practice of Constraint Programming  CP 2002, Lecture Notes in Computer Science, 2470, Springer Berlin Heidelberg, pp. 714–719, doi:10.1007/3540461353_51, ISBN 9783540441205
 ↑ Arbelaez, Alejandro; Hamadi, Youssef (2011), "Improving Parallel Local Search for SAT", Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 46–60, doi:10.1007/9783642255663_4, ISBN 9783642255656
References are ordered by date of publication:
 Michael R. Garey & David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NPCompleteness. W.H. Freeman. ISBN 0716710455. A9.1: LO1 – LO7, pp. 259 – 260.
 MarquesSilva, J.; Glass, T. (1999). "Combinational equivalence checking using satisfiability and recursive learning" (PDF). Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078) (PDF). p. 145. doi:10.1109/DATE.1999.761110. ISBN 0769500781.
 Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19: 7–34. doi:10.1023/A:1011276507260. S2CID 2484208.
 Giunchiglia, E.; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando (eds.). Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science. 2919. doi:10.1007/b95238. ISBN 9783540208518. S2CID 31129008.
 Babic, D.; Bingham, J.; Hu, A. J. (2006). "BCubing: New Possibilities for Efficient SATSolving" (PDF). IEEE Transactions on Computers. 55 (11): 1315. doi:10.1109/TC.2006.175. S2CID 14819050.
 Rodriguez, C.; Villagra, M.; Baran, B. (2007). "Asynchronous team algorithms for Boolean Satisfiability" (PDF). 2007 2nd BioInspired Models of Network, Information and Computing Systems. pp. 66–69. doi:10.1109/BIMNICS.2007.4610083. S2CID 15185219.
 Carla P. Gomes; Henry Kautz; Ashish Sabharwal; Bart Selman (2008). "Satisfiability Solvers". In Frank Van Harmelen; Vladimir Lifschitz; Bruce Porter (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. 3. Elsevier. pp. 89–134. doi:10.1016/S15746526(07)030027. ISBN 9780444522115.
 Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
External linksEdit
Wikimedia Commons has media related to [[commons:Lua error in Module:WikidataIB at line 506: attempt to index field 'wikibase' (a nil value).Lua error in Module:WikidataIB at line 506: attempt to index field 'wikibase' (a nil value).]]. 
 SAT Game  try solving a Boolean satisfiability problem yourself
SAT problem formatEdit
A SAT problem is often described in the DIMACSCNF format: an input file in which each line represents a single disjunction. For example, a file with the two lines
1 5 4 0 1 5 3 4 0
represents the formula "(x_{1} ∨ ¬x_{5} ∨ x_{4}) ∧ (¬x_{1} ∨ x_{5} ∨ x_{3} ∨ x_{4})".
Another common format for this formula is the 7bit ASCII representation "(x1  ~x5  x4) & (~x1  x5  x3  x4)".
 BCSAT is a tool that converts input files in humanreadable format to the DIMACSCNF format.
Online SAT solversEdit
 BoolSAT – Solves formulas in the DIMACSCNF format or in a more humanfriendly format: "a and not b or a". Runs on a server.
 Logictools – Provides different solvers in javascript for learning, comparison and hacking. Runs in the browser.
 minisatinyourbrowser – Solves formulas in the DIMACSCNF format. Runs in the browser.
 SATRennesPA – Solves formulas written in a userfriendly way. Runs on a server.
 somerby.net/mack/logic – Solves formulas written in symbolic logic. Runs in the browser.
Offline SAT solversEdit
 MiniSAT – DIMACSCNF format and OPB format for its companion PseudoBoolean constraint solver MiniSat+
 Lingeling – won a gold medal in a 2011 SAT competition.
 PicoSAT – an earlier solver from the Lingeling group.
 Sat4j – DIMACSCNF format. Java source code available.
 Glucose – DIMACSCNF format.
 RSat – won a gold medal in a 2007 SAT competition.
 UBCSAT. Supports unweighted and weighted clauses, both in the DIMACSCNF format. C source code hosted on GitHub.
 CryptoMiniSat – won a gold medal in a 2011 SAT competition. C++ source code hosted on GitHub. Tries to put many useful features of MiniSat 2.0 core, PrecoSat ver 236, and Glucose into one package, adding many new features
 Spear – Supports bitvector arithmetic. Can use the DIMACSCNF format or the Spear format.
 HyperSAT – Written to experiment with Bcubing search space pruning. Won 3rd place in a 2005 SAT competition. An earlier and slower solver from the developers of Spear.
 BASolver
 ArgoSAT
 Fast SAT Solver – based on genetic algorithms.
 zChaff – not supported anymore.
 BCSAT – humanreadable boolean circuit format (also converts this format to the DIMACSCNF format and automatically links to MiniSAT or zChaff).
 gini – Go language SAT solver with related tools.
 gophersat – Go language SAT solver that can also deal with pseudoboolean and MAXSAT problems.
 CLP(B) – Boolean Constraint Logic Programming, for example SWIProlog.
SAT applicationsEdit
 WinSAT v2.04: A Windowsbased SAT application made particularly for researchers.
ConferencesEdit
PublicationsEdit
BenchmarksEdit
SAT solving in general:
Evaluation of SAT solversEdit
 Yearly evaluation of SAT solvers
 SAT solvers evaluation results for 2008
 International SAT Competitions
 History
More information on SAT:
This article includes material from a column in the ACM SIGDA enewsletter by Prof. Karem Sakallah
Original text is available here