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 truth-values can be assigned to its free variables in a way that makes the formula true. The class of satisfiable propositional formulae is NP-complete, as is that of its variant 3-satisfiability. (Other variants, such as 2-satisfiability and Horn-satisfiability, 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.

Table of contents

1 Complexity
2 Restrictions of SAT

2.1 3-satisfiability

3 Extensions of SAT

3.2 Proof of NP-completeness

4 Algorithms for solving SAT
5 External links

Complexity

SAT is NP-complete. In fact, it was the first known NP-complete problem, as proved by Stephen Cook in 1971. The problem remains NP-complete even if all expressions are written in conjunctive normal form with 3 variables per clause (3-CNF). This means the expression has the form:

(x₁₁ OR x₁₂ OR x₁₃) AND

(x₂₁ OR x₂₂ OR x₂₃) AND

(x₃₁ OR x₃₂ OR x₃₃) AND ...

where each x is a variable, with or without a NOT in front of it, and each variable can appear multiple times in the expression.

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 there is a clause which does not contain x and NOT x, and 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. Also this problem can be solved in polynomial time. Note that this does not prove that DNF-SAT and 2SAT are not NP-complete but only that if they are then the Complexity classes P and NP are equal.

3-satisfiability

It is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains at most k = 3 literals.

for example :

E = (x1 or ~x2 or ~x3) and (x1 or x2 or x4)

E has two clauses (denoted by parentheses), four literals (x1, x2, x3, x4), 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 (x1 through x4) such that the entire expression is TRUE. In this instance, there is such an assignment (for example, x1 = TRUE, x2 = TRUE, x3=TRUE, x4=TRUE), so the answer to this instance is YES. If there were no such assignment, the answer would be NO.

Since k-SAT (the general case) reduces to 3-SAT, and 3-SAT is known to be NP-complete, it can be used to prove that other problems are also NP-complete. 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:

In this case the problem is called QBF (Quantified Boolean Formula) and it can be shown to be PSPACE-Complete. That is widely thought to be much harder than NP-complete, though that has not yet been proved.

Proof of NP-completeness

We give here a sketch of the proof of NP-completeness. To prove that SAT is NP-complete we must show that

SAT is in NP, and
all other NP problems can be reduced to it in polynomial time.

First, notice that it is easy to verify a YES answer: simply plug in a given set of variable values and see if they make the expression true. Therefore the problem is in NP.

Next, consider an arbitrary problem X that is in NP. By definition, there must be an algorithm for checking certificates for YES answers to X in polynomial time. Given such an algorithm it is possible to construct a polynomial-time algorithm that, given the size of the certificate, constructs a boolean circuit that is polynomially large in the certificate size and decides whether its input is a binary encoding of a valid certificate or not. This circuit can then be transformed by another polynomial-time algorithm into an equivalent boolean formula that is still polynomially large in the certificate size. It then holds that this formula is satisfiable iff there is a valid certificate, which means that we have reduced the original problem to SAT.

Algorithms for solving SAT

There are two classes of high-performance algorithms for solving instances of SAT in practice: modern variants of the David-Putnam-Loveland algorithm, such as zchaff, 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 second-order logic, constraint satisfaction problems, 0-1 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.

Compare with: decision problem