Boolean satisfiability problem

The satisfiability problem of propositional logic (SAT, satisfiability of English ) is a decision problem. It asks whether a propositional formula is satisfiable. Applications can be found among others in complexity theory, verification and design of logic circuits. In particular in complexity theory is referred to as satellite only the specific case of the formulas which are present in conjunctive normal form.

The satisfiability problem of propositional logic is decidable in the number of variables in exponential time, for example by setting up a truth table. Whether there is also an algorithm that solves SAT in polynomial time, is not known. The research deals with the development of highly efficient method (so-called SAT - solvers ). Well-known SAT solvers are Binary decision diagrams, or the Davis -Putnam procedure. Some solvers use stochastic or systematic search method for deciding the satisfiability. The best known and most widely used method for the systematic search is (as of 2008 ), the DPLL procedure ( Davis - Putnam - Logemann - Loveland ), which has been greatly improved in recent decades with the help of heuristics and learning techniques.

SAT belongs to the class of problems that can be solved in polynomial time by a nondeterministic Turing machine. The unresolved question is whether SAT can be solved by a deterministic Turing machine (ie with a conventional computer ) in polynomial time, can be formulated as: Applies?

The satisfiability problem of propositional logic is NP -complete. This implies that any problem can be from recycled in polynomial time to SAT ( Polynomialzeitreduktion ). In the early 1970s showed Stephen A. Cook and Leonid Levin independently this property, known as the set of Cook. Cook showed this to an algorithm that formulates the computation steps of a non- deterministic Turing machine in propositional logic and thus can be reduced to SAT. Richard M. Karp showed in 1972, the NP- completeness of other problems. He coined so that the current understanding of NP- completeness.

Thus, if applies, then each problem of in, that is, the following applies. The reverse direction of the implication is true. The P- NP problem " is true or not?" Is one of the great unsolved questions of complexity theory. Once a problem is NP-complete, we may assume that the search for a polynomial time algorithm for this is hopeless. To follow this assumption means nothing more than the conviction of many mathematicians, that does not apply to share.

Variants of SAT

SAT can be varied in many ways by restrictions and generalizations. The problem 3-SAT is a variant that contains at most three literals per clause. Despite the limitation, 3-SAT is NP- complete, for SAT can be reduced to 3-SAT in polynomial time.

Each 3-SAT with variables p and q clauses can be mapped on a graph G with p q nodes, where all variable nodes are connected with those of clause nodes in which they occur. A formula in P3SAT when it is in the 3- SAT, and the graph is planar. Also P3SAT is NP -complete.

The problem MAX - SAT is to determine the maximum number of satisfiable clauses of a formula. It is PP -complete. MAJ - SAT, the decision problem whether a propositional formula is satisfied by more than half of all possible allocations is also PP -complete.

There are variants of SAT that are complete with respect to these classes to many other complexity classes. For example, the variant 2- SAT is NL -complete. The HORNSAT problem is P -complete. The extension of propositional logic formulas by introducing quantifiers leads to QBF (also called QSAT ), a PSPACE - complete problem.

Finally, one can combine SAT with other decision theories. The resulting problem is called an SMT problem ( Satisfiability Modulo Theory) and can be solved eg by coding in a pure SAT - problem, or by a combination of decision procedures.