Boolean satisfiability problem

The Boolean satisfiability problem (SAT) is a decision problem considered in complexity theory. An instance of the problem is defined by 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?
In mathematics, a formula of propositional logic is said to be satisfiable if truthvalues can be assigned to its free variables in a way that makes the formula true. The class of satisfiable propositional formulae is NPcomplete, as is that of its variant 3satisfiability. (Other variants, such as 2satisfiability and Hornsatisfiability, can be solved by efficient algorithms.)
The propositional satisfiability problem (SAT), which is given a propositional formula is to decide whether or not it is satisfiable, is of central importance in various areas of computer science, including theoretical computer science, algorithmics, artificial intelligence, hardware design and verification.
Contents 
Complexity
SAT is NPcomplete. In fact, it was the first known NPcomplete problem, as proved by Stephen Cook in 1971 (see Cook's theorem for the proof). Until that time, it was not known that NPcomplete problems even existed. The problem remains NPcomplete even if all expressions are written in conjunctive normal form with 3 variables per clause (3CNF), yielding the 3SAT problem. This means the expression has the form:
 (x_{11} OR x_{12} OR x_{13}) AND
 (x_{21} OR x_{22} OR x_{23}) AND
 (x_{31} OR x_{32} OR x_{33}) 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 3colorings, the SAT formula produced by the reduction will have 17 satisfying assignments.
Restrictions of SAT
SAT seems to become easier if the formulas are restricted to those in disjunctive normal form, where each clause is an AND of variables (some with NOTs), and all the clauses are ORed together. This is because such a formula is satisfiable iff some clause is satisfiable, and a conjunctive clause is satisfiable iff it does not contain both x and NOT x for some variable x. This can be checked in polynomial time.
SAT also seems to be 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 exclusiveor 2satisfiability, 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 polynomialtime unification algorithm, and is in fact Pcomplete. 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 NPcomplete, unlike SAT. We don't yet know this for certain, however.
3satisfiability
3satisfiability is a special case of ksatisfiability (kSAT) or simply satisfiability (SAT), when each clause contains at most k = 3 literals. It was one of Karp's 21 NPcomplete problems.
Here is an example, where ~ indicates NOT:
 E = (x_{1} or ~x_{2} or ~x_{3}) and (x_{1} or x_{2} or x_{4})
E has two clauses (denoted by parentheses), four literals (x_{1}, x_{2}, x_{3}, x_{4}), 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_{1} through x_{4}) such that the entire expression is TRUE. In this instance, there is such an assignment (for example, x_{1} = TRUE, x_{2} = TRUE, x_{3}=TRUE, x_{4}=TRUE), so the answer to this instance is YES. If there were no such assignment, the answer would be NO.
Since kSAT (the general case) reduces to 3SAT, and 3SAT can be proven (http://cs482.elliottback.com/archives/2005/03/16/lecture233sat/) to be NPcomplete, it can be used to prove that other problems are also NPcomplete. This is done by showing how a solution to another problem could be used to solve 3SAT. An example of a problem where this method has been used is "Clique".
Extensions of SAT
The satisifiability problem seems to become more difficult if we allow quantifiers such as "for all" and "there exists" that bind the boolean variables. An example of such an expression would be:
 <math>\forall x, \exists y,\exists z; (x \lor y \lor z) \land (\lnot x \lor \lnot y \lor \lnot z)<math>
If we use only <math>\exists<math> quantifiers, this is still the SAT problem. If we allow only <math>\forall<math> quantifiers, it becomes the CoNPcomplete TAUTOLOGY problem. If we allow both, 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.
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. UNIQUESAT 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 polynomialtime) algorithm to solve this problem, then all problems in NP can be solved just as easily.
MaxSAT, 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 NPhard to solve exactly.
Algorithms for solving SAT
There are two classes of highperformance algorithms for solving instances of SAT in practice: modern variants of the DavisLogemannLoveland algorithm, such as Chaff, and stochastic local search algorithms, such as WalkSAT. Particularly in hardware design and verification applications, satisfiability and other logical properties of a given propositional formula are often decided based on a representation of the formula as a binary decision diagram (BDD).
Propositional satisfiability has various generalisations, including satisfiability for quantified Boolean formulae, for first and secondorder logic, constraint satisfaction problems, 01 integer programming, and maximum satisfiability.
Many other decision problems, such as graph colouring problems, planning problems, and scheduling problems can be rather easily encoded into SAT.
External links
 http://www.satlib.org
 http://www.satlive.org/index.jsp
 Forced Satisfiable SAT Benchmarks (http://www.nlsde.buaa.edu.cn/~kexu/benchmarks/benchmarks.htm)
de:Erfüllbarkeitsproblem der Aussagenlogik es:Problema de satisfacibilidad booleana th:ปัญหาความสอดคล้องแบบบูล