Satisfiability problem of propositional logic

The satisfiability problem of propositional logic ( SAT , from English satisfiability 'satisfiability') is a decision problem . It asks whether a propositional formula can be fulfilled . Applications can be found in complexity theory , verification and the design of logic circuits . In complexity theory in particular, SAT is only used to designate the special case of formulas that are in conjunctive normal form.

The satisfiability of propositional logic is in exponential time in the number of variables determinable , for example by setting up a truth table . It is not known whether there is also an algorithm that solves SAT in polynomial time. Research deals with the development of the most efficient methods possible (so-called SAT solvers ). Well-known SAT solvers are binary decision diagrams or the Davis-Putnam method . Some solvers use stochastic or systematic search methods to decide whether they can be satisfied. The best known and most widespread method for systematic search is (as of 2008) the DPLL method (Davis-Putnam-Logemann-Loveland), which has been greatly improved in the last few decades with the help of heuristics and learning methods.

SAT belongs to the class of problems that can be solved in polynomial time with a nondeterministic Turing machine . The still unsolved question of whether SAT can also be solved with a deterministic Turing machine (i.e. with a conventional computer) in polynomial time can be formulated as: Is it true ? ${\displaystyle {\mathcal {NP}}}$ ${\displaystyle {\mbox{SAT}}\in {\mathcal {P}}}$

The satisfiability problem in propositional logic is NP-complete . This means that every problem in polynomial time can be traced back to SAT ( polynomial time reduction ). In the early 1970s , Stephen A. Cook and Leonid Levin independently exhibited this property known as Cook's Theorem . For this purpose Cook showed an algorithm with which the calculation steps of a non-deterministic Turing machine can be formulated in propositional logic and thus reduced to SAT. In 1972 Richard M. Karp showed the NP-completeness of further problems . He thus shaped today's understanding of NP completeness. ${\displaystyle {\mathcal {NP}}}$

So if holds, then every problem from is also in , that is, then holds . The reverse of the implication also applies. The P-NP problem “applies or not?” Is one of the great unsolved questions in complexity theory. Many mathematicians believe that it doesn't. If a problem is NP-complete, one can assume in this case that the search for a polynomial time algorithm is futile. ${\displaystyle {\mbox{SAT}}\in {\mathcal {P}}}$ ${\displaystyle {\mathcal {NP}}}$ ${\displaystyle {\mathcal {P}}}$ ${\displaystyle {\mathcal {P}}={\mathcal {NP}}}$ ${\displaystyle {\mathcal {P}}={\mathcal {NP}}}$ ${\displaystyle {\mathcal {P}}={\mathcal {NP}}}$

Variants of SAT

SAT can be varied in many ways through limitations and generalizations. Problem 3-SAT is a variant that contains at most three literals per clause. Despite the restriction, 3-SAT is also NP-complete, because SAT can be reduced to 3-SAT in polynomial time .

Every 3-SAT with p variables and q clauses can be mapped onto a graph G with p + q nodes , in which all variable nodes are connected to those clause nodes in which they occur. A formula is in P3SAT when it is in 3-SAT and the graph is planar . P3SAT is also NP-complete.

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

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

Finally, SAT can also be coupled with other decision theories. The resulting problem is known as an SMT (Satisfiability Modulo Theory) problem and can e.g. B. can be solved by coding in a pure SAT problem or by a combination of decision-making processes.

See also

• Resolution (logic)
• Satisfiability problem for circuits

Individual evidence

1. ^ ^{A b} Daniel Pierre Bovet and Pierluigi Crescenzi: Introduction to the Theory of Complexity . Prentice Hall, 1994, ISBN 0-13-915380-2 , pp. 199 .

literature

• Christos H. Papadimitriou: Computational Complexity . Addison-Wesley, ISBN 978-0-201-53082-7