Boolean satisfiability problem

The satisfiability problem of propositional logic (SAT) is a decision problem in theoretical computer science. It deals with the question whether a given propositional formula is satisfiable. In other words, does an assignment of the variables of with the values true or false exist such that evaluates to true?

SAT belongs to the complexity class NP of problems that can be solved by a nondeterministic Turing machine in polynomial time. Moreover, SAT was the first problem for which NP-completeness was proved (Cook's theorem). Thus, any problem from NP can be reduced to SAT in polynomial time (polynomial time reduction). NP-complete problems thus provide a kind of upper bound on the difficulty of problems in NP.

A deterministic Turing machine (such as a conventional computer) can decide SAT in exponential time, for example by constructing a truth table. No efficient algorithm for SAT is known, and it is generally conjectured that such a polynomial-time algorithm does not exist. The question of whether SAT can be solved in polynomial time is equivalent to the P-NP problem, one of the best known open problems in theoretical computer science

Much of the research is concerned with developing the most efficient methods possible for solving SAT in practice (so-called SAT solvers). Modern SAT solvers can solve instances of medium difficulty with hundreds of millions of variables or clauses in a feasible time. This is sufficient for practical applications, e.g., in formal verification, artificial intelligence, electronic design automation, and various planning and scheduling algorithms.

Terminology

A propositional formula consists of variables, parentheses, and the propositional conjunctions conjunction ("and", often notated ∧), disjunction ("or", ∨), and negation ("not", ¬). A variable can take either the value true or the value false. A literal is an occurrence of a variable (positive literal) or its negation (negative literal). A literal is called pure if it occurs in only one occurrence, that is, either positive or negative. A monomial is a finite set of literals that are exclusively conjunctively connected. A clause is a finite set of literals that are exclusively disjunctively linked. A unit clause is a clause consisting of only a single literal. A Horn clause is a clause with at most one positive literal.

A propositional formula is in conjunctive normal form (KNF) if it consists only of conjunctions of clauses. A Horn formula is in conjunctive normal form if it consists solely of Horn clauses. The formula $(x_{1}\lor \lnot x_{2})\land (\lnot x_{1}\lor x_{2}\lor x_{3})\land \lnot x_{1}$ is in conjunctive normal form. However, since only the first and third clauses are Horn clauses, it is not a Horn formula. The third clause is a unit clause.

A propositional formula is in disjunctive normal form (DNF) if it consists only of disjunctions of monomials. The formula $(x_{1}\land \lnot x_{2})\lor (\lnot x_{1}\land x_{2}\land x_{3})\lor \lnot x_{1}$ is in disjunctive normal form.

Definition and variants

A formula is called satisfiable if and only if there exists an assignment of values true or false to each variable such that the formula is true. Formally, SAT is defined as the formal language

$SAT=\{F\ |\ F$ is propositional formula and satisfiable $\}$

In practice, SAT is usually understood as the problem of finding out whether a formula satisfiable. There are numerous variants and for most complexity classes there exists a variant of SAT which is complete with respect to this class.

Polynomial decidable variants of SAT

HORNSAT restricts SAT to Horn formulas given in disjunctive normal form. HORNSAT is P-complete
DNF-SAT restricts SAT to formulas given in disjunctive normal form. DNF-SAT is decidable in polynomial time, since a formula given in DNF is satisfiable exactly if none of its monomials contains two complementary literals
2-SAT restricts SAT to formulas whose clauses contain at most 2 literals. 2-SAT is decidable in linear time.

3-SAT

The problem 3-SAT restricts the number of literals to 3 literals per clause. Despite this restriction, 3-SAT is NP-complete since SAT can be reduced to 3-SAT in polynomial time. The same is true for all problems k-SAT with k > 3.

P3-SAT

An instance of problem 3-SAT consisting of p variables and q clauses can also be represented by means of a graph with (p + q) many nodes. A formula is in P3-SAT if it is in 3-SAT and this graph is planar. P3-SAT is NP-complete.

MAX-SAT and MAJ-SAT

The MAX-SAT problem is to determine the maximum number of satisfiable clauses of a given formula. MAX-SAT is NP-complete and even APX-complete. It follows that no PTAS can exist for MAX-SAT if P ≠ NP.

MAJ-SAT

MAJ-SAT is the problem of deciding whether the majority of all possible variable assignments satisfy the formula. MAJ-SAT is PP-complete.

QBF (QSAT)

QBF generalizes SAT for quantified propositional formulas, that is, formulas that contain quantifiers. QBF is PSPACE-complete.