Satisfiability problem

From Glossary

Jump to: navigation, search

(SAT). Find a truth assignment to logical propositions such that a (given) collection of clauses is true (or ascertain that at least one clause must be false in every truth assignment). This fundamental problem in computational logic forms the foundation for NP-completeness. When SAT is in conjunctive normal form and may not be satisfiable, we define the problem of maximizing the number of true clauses as MAXSAT.


Problems are divided into two categories: those for which there exists an algorithm to solve it with polynomial time complexity, and those for which there is no such algorithm. We denote the former class of problems by LaTeX: P. There are problems for which no known algorithm exists that solves it in polynomial time, but there is also no proof that no such algorithm exists. Among these problems that are not known to be in LaTeX: P (or in LaTeX: ~P), there is a subclass of problems known as NP-complete: those for which either all are solvable in polynomial time, or none are. Formally, a problem is NP if there exists an algorithm with polynomial time complexity that can certify a solution. For example, it is not known whether there exists a polynomial algorithm to solve a system of Diophantine equations, LaTeX: \textstyle Ax=b \mbox{ for } x \in \mathbb{Z}^n (integer n-vectors). However, we can certify any trial LaTeX: x in polynomial time, just by checking that it is in LaTeX: \textstyle \mathbb{Z}^n, then multiplying by LaTeX: A to compare with LaTeX: b. A problem, LaTeX: p, is NP-complete if it is NP and for any problem in NP, there exists a polynomial time algorithm to reduce it to LaTeX: p. A fundamental member of the NP-complete class is the satisfiability problem. It is an open question whether LaTeX: P=\mbox{NP}, and most regard the NP-complete problems as having exponential time complexity. Further details are in the supplement, Introduction to Computational Complexity.

Personal tools