Discover

'Satisfiability' is the problem of determining if the variables of a given
Boolean formula can be assigned in such a way as to make the formula
evaluate to TRUE. Equally important is to determine that no such assignments
exist, implying that the function expressed by the formula is identically FALSE
for all possible variable assignments. In this latter case, we would say
that the function is unsatisfiable; otherwise it is satisfiable. To emphasize
the binary nature of this problem, it is frequently referred to as 'Boolean'
or 'propositional satisfiability'. The shorthand "SAT" is also commonly used
to denote it, with the implicit understanding that the function and its variables
are all binary-valued.

Contents

Basic definitions, terminology and applications

Complexity and restricted versions

NP-completeness

2-satisfiability

3-satisfiability

Horn-satisfiability

Schaefer's dichotomy theorem

Extensions of SAT

Algorithms for solving SAT

References

External links

Basic definitions, terminology and applications

In complexity theory, the 'Boolean satisfiability problem (SAT)'
is a decision problem, whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses.
The question is: given the expression, is there some assignment of ''TRUE'' and ''FALSE'' values to the variables that will
make the entire expression true? A formula of propositional logic is said to be 'satisfiable' if logical values can be assigned to its variables in a way that makes the formula true. The class of satisfiable propositional formulas is NP-complete. The propositional satisfiability problem (SAT), which decides whether a given propositional formula is satisfiable, is of central importance in various areas of computer science, including theoretical computer science, algorithmics, artificial intelligence, hardware design and verification.
The problem can be significantly restricted while still remaining NP-complete. By applying De Morgan's laws, we can assume that NOT operators are only applied directly to variables, not expressions; we refer to either a variable or its negation as a ''literal''. For example, both ''x''₁ and not(''x''₂) are literals, the first a ''positive'' literal and the second a ''negative'' literal. If we OR together a group of literals, we get a ''clause'', such as (''x''₁ ''or'' not(''x''₂)). Finally, let us consider formulas that are a conjunction (AND) of clauses - this is the conjunctive normal form (CNF). Determining whether a formula in this form is satisfiable is still NP-complete, even if each clause is limited to at most three literals. This last problem is called 3SAT, 3CNFSAT, or 3-satisfiability.
On the other hand, if we restrict each clause to at most two literals, the resulting problem, 2SAT, is 'NL'-complete. Alternately, if every clause must be a Horn clause, containing at most one positive literal, the resulting problem, Horn-satisfiability, is 'P'-complete.
Cook's theorem proves that the Boolean satisfiability problem is NP-complete,
and in fact, this was the first decision problem proved to be NP-complete.
However, beyond this theoretical significance, efficient and
scalable algorithms for SAT that were developed over the last decade have
contributed to dramatic advances in our ability to automatically solve problem
instances involving tens of thousands of variables and millions of
constraints. Examples of such problems in Electronic Design Automation EDA include
routing of FPGAs, combinational equivalence checking, model checking,
formal verification of pipelined microprocessors, logic synthesis, etc.
In fact, a SAT-solving engine is now considered to be an essential component in the EDA
toolbox and all EDA vendors provide such a capability (usually behind the
scenes.)

Complexity and restricted versions

NP-completeness

SAT was the first known 'NP'-complete problem, as proved by Stephen Cook in 1971 (see Cook's theorem for the proof). Until that time, the concept of an NP-complete problem did not even exist. The problem remains 'NP'-complete even if all expressions are written in ''conjunctive normal form'' with 3 variables per clause (3-CNF), yielding the '3SAT' problem. This means the expression has the form:
:(''x''₁₁ OR ''x''₁₂ OR ''x''₁₃) AND
:(''x''₂₁ OR ''x''₂₂ OR ''x''₂₃) AND
:(''x''₃₁ OR ''x''₃₂ OR ''x''₃₃) AND ...
where each ''x'' is a variable or a negation of a variable, and each variable can appear multiple times in the expression.
A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, if a graph has 17 valid 3-colorings, the SAT formula produced by the reduction will have 17 satisfying assignments.

2-satisfiability

Main articles: 2-satisfiability

SAT is easier if the formulas are restricted to those in disjunctive normal form, that is, they are disjunction (OR) of terms, where each term is a conjunction (AND) of literals (possibly negated variables). Such a formula is indeed satisfiable if and only if at least one of its terms is satisfiable, and a term is satisfiable if and only if it does not contain both ''x'' and NOT ''x'' for some variable ''x''. This can be checked in polynomial time.
SAT is also easier if the number of literals in a clause is limited to 2, in which case the problem is called 2SAT. This problem can also be solved in polynomial time, and in fact is complete for the class NL. Similarly, if we limit the number of literals per clause to 2 and change the AND operations to XOR operations, the result is ''exclusive-or 2-satisfiability'', a problem complete for SL = L.
One of the most important restrictions of SAT is HORNSAT, where the formula is a conjunction of Horn clauses. This problem is solved by the polynomial-time Horn-satisfiability algorithm, and is in fact P-complete. It can be seen as P's version of the boolean satisfiability problem.
Provided that the complexity classes P and NP are not equal, none of these restrictions are NP-complete, unlike SAT. The assumption that P and NP are not equal is not currently proved.

3-satisfiability

3-satisfiability is a special case of ''k''-satisfiability (''k''-SAT) or simply satisfiability (SAT), when each clause contains exactly ''k'' = 3 literals. It was one of Karp's 21 NP-complete problems.
Here is an example, where ~ indicates NOT:
: E = (''x''₁ or ~''x''₂ or ~''x''₃) and (''x''₁ or ''x''₂ or ''x''₄)
E has two clauses (denoted by parentheses), four literals (''x''₁, ''x''₂, ''x''₃, ''x''₄), and ''k''=3 (three literals per clause).
To solve this instance of the decision problem we must determine whether there is a truth value (TRUE or FALSE) we can assign to each of the literals (''x''₁ through ''x''₄) such that the entire expression is TRUE. In this instance, there is such an assignment (''x''₁ = TRUE, ''x''₂ = TRUE, ''x''₃=TRUE, ''x''₄=TRUE), so the answer to this instance is YES. This is one of many possible assignments, with for instance, any set of assignments including ''x''₁ = TRUE being sufficient. If there were no such assignment(s), the answer would be NO.
Since k-SAT (the general case) reduces to 3-SAT, and 3-SAT can be proven to be NP-complete, it can be used to prove that other problems are also NP-complete. This is done by showing how a solution to another problem could be used to solve 3-SAT. An example of a problem where this method has been used is "Clique". It's often easier to use reductions from 3-SAT than SAT to problems which researchers are attempting to prove NP-complete.
3-SAT can be further restricted to One-in-three 3SAT, where we ask if ''exactly'' one of the variables in each clause is true, rather than ''at least'' one. One-in-three 3SAT remains NP-complete.

Horn-satisfiability

Main articles: Horn-satisfiability

A clause is Horn if it contains at most one positive literal. Such clauses are of interest because they are able to express entailment of one variable from a set of other variables. Indeed, one such clauses $$
eg x_1 ee cdots ee
eg x_n ee y can be rewritten as $x\_1\; wedge\; cdots\; wedge\; x\_n$
ightarrow y, that is, if $x\_1,ldots,x\_n$ are all true, then $y$ needs to be true as well.
The problem of deciding whether a set of Horn clauses is satisfiable is in P. This problem can indeed be solved by a single step of the Unit propagation, which produces the single minimal (w.r.t. the set of literal assigned to true) model of the set of Horn clauses.
A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. 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.

Schaefer's dichotomy theorem

Main articles: Schaefer's dichotomy theorem

The restrictions above (CNF, 2CNF, 3CNF, Horn) bound the considered formulae to be conjunction 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 either in P or NP-complete. The membership in P of the satisfiability of 2CNF and Horn formulae are special cases of this theorem.

Extensions of SAT

An extension that has gained significant popularity since 2003 is Satisfiability modulo theories
that can enrich CNF formulas with linear constraints, arrays, all-different constraints, uninterpreted functions, 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 seems to become more difficult (PSPACE-complete) if we allow ''quantifiers'' such as "for all" and "there exists" that bind the boolean variables. An example of such an expression would be:
:
If we use only $exists$ quantifiers, this is still the SAT problem. If we allow only quantifiers, it becomes the Co-NP-complete tautology problem. If we allow both, the problem is called the quantified boolean formula problem (QBF), which can be shown to be PSPACE-complete. It is widely believed that PSPACE-complete problems are strictly harder than any problem in NP, although this has not yet been proved.
A number of variants deal with the number of variable assignments making the formula true. Ordinary SAT asks if there is at least one such assignment. MAJSAT, which asks if the majority of all assignments make the formula true, is complete for PP, a probabilistic class. The problem of how many variable assignments satisfy a formula, not a decision problem, is in #P. UNIQUE-SAT or USAT is the problem of determining whether a formula known to have either zero or one satisfying assignments has zero or has one. Although this problem seems easier, it has been shown that if there is a practical (randomized polynomial-time) algorithm to solve this problem, then all problems in NP can be solved just as easily.
The maximum satisfiability problem, an FNP generalization of SAT, asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient approximation algorithms, but is NP-hard to solve exactly. Worse still, it is APX-complete, meaning there is no polynomial-time approximation scheme (PTAS) for this problem unless P=NP.

Algorithms for solving SAT

There are two classes of high-performance algorithms for solving instances of SAT in practice:
modern variants of the DPLL algorithm, such as Chaff or GRASP,
and stochastic local search algorithms, such as WalkSAT.
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 60s (see references below) and is now commonly referred to as the
Davis-Putnam-Logemann-Loveland (DPLL) algorithm. Modern SAT solvers (developed
in the last ten years) augment the basic DPLL search algorithm with efficient
conflict analysis, clause learning, non-chronological backtracking (aka
backjumping), as well as "two-watched-literals" 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 EDA. 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 in the public domain, and are
remarkably easy to use. In particular, MiniSAT,
which won the 2005 SAT competition, only has about 600 lines of code.
Genetic algorithms and other general-purpose stochastic local search methods are also being used to solve SAT problems, especially when there is no or limited knowledge of the specific structure of the problem instances to be solved. 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).
Propositional satisfiability has various generalisations, including satisfiability for quantified boolean formula problem, for first- and second-order logic, constraint satisfaction problems, 0-1 integer programming, and maximum satisfiability problem.
Many other decision problems, such as graph colouring problems, planning problems, and scheduling problems, can be easily encoded into SAT.

References

# M. Davis and H. Putnam, , Journal of the Association for Computing Machinery, vol. 7, no., pp. 201-215, 1960.
# M. Davis, G. Logemann, and D. Loveland, , Communications of the ACM, vol. 5, no. 7, pp. 394-397, 1962.
# S. A. Cook, , in Proc. 3rd Ann. ACM Symp. on Theory of Computing, pp. 151-158, Association for Computing Machinery, 1971.
#