1. Overview
The Boolean Satisfiability Problem or in other words SAT is the first problem that was shown to be NP-Complete. In this tutorial, we’ll discuss the satisfiability problem in detail and present the Cook-Levin theorem.
Furthermore, we’ll discuss the 3-SAT problem and show how it can be proved to be NP-complete by reducing it to the SAT problem.
2. Introduction to SAT
In this section, we’ll discuss a general definition of the SAT problem.
A given boolean expression, determining if there exists a truth assignment to its variables for which the expression is true is defined as the satisfiability problem.
Let’s take an example to discuss further.
a
b
c
1
1
1
1
0
0
1
1
1
0
0
0
1
1
0
0
1
0
0
0
1
0
1
1
0
1
0
0
0
0
1
0
1
1
0
0
0
0
0
0
We’ve taken two expressions here. To test whether there exists a truth assignment to variables , , , we’ve tested all possible assignments.
There are satisfying truth assignments for the expression above and hence it is satisfiable.
But the expression is false for all possible truth assignments and hence it is unsatisfiable.
This takes . This is called the truth table method. If there are variables in the boolean expression, then the truth table method would take time to determine if there is a truth assignment that makes the expression true.
3. Conjunctive Normal Form (CNF)
When we’re discussing the SAT problem, it’s essential to know about the conjunctive normal form (CNF). In this section, we’ll see a short description of the CNF concept.
A boolean expression is said to be in CNF form if it’s a conjunction of a set of clauses, where each clause is defined as a disjunction (logical OR) of literals. We can define a literal as a variable or a negation of a variable. In the above example are all literals.
Every boolean expression can be expressed as a CNF by repeatedly using De Morgan’s Laws, the law of double negation and distributive laws under AND and OR:
where,
The above CNF is a -CNF, that is, it has a maximum of literals in every clause. We pick each literal from a set of variables:
4. SAT Variants
There are a number of SAT variants. In this section, we’ve listed out few.
4.1. 2-SAT
In the 2-SAT problem, every clause has two literals and is solvable in a polynomial-time problem.
We can pick a variable , and then assign true. We assign true to the other variable of all the clauses with . If those clauses are satisfied, then we pick the remaining clauses which don’t have or and continue the process.
On the other side, if the clauses with are not all satisfied at this point, then we assign false to and repeat the above process. If all the clauses containing and are all not satisfied, then the 2-SAT is unsatisfiable.
An important application of 2-SAT is to identify an undirected graph that can be represented as a complete bipartite graph and independent set. This helps to identify the business relationships among autonomous subsystems of the internet.
Many algorithms for the automatic label placement problem use the 2-SAT concept.
4.2. Weighted 2-SAT
Given a CNF with literals per clause and an integer , the problem of determining if there is a truth assignment with at most variables set to true for which the CNF is satisfiable.
This problem is NP-Complete. Many algorithms use the weighted 2-SAT concept for solving the vertex cover problem.
4.3. 3-SAT
In the 3-SAT problem, each clause has at most literals. This problem is NP-Complete.
The 3-SAT problem is part of the Karp’s 21 NP-complete problems and is used as the starting point to prove that the other problems are also NP-Complete. One example is the independent set problem. The Independent Set Problem can be shown to be NP-Complete by showing that the 3-SAT is polynomially reducible to an independent set problem.
4.4. Exactly One 3-SAT
Each clause in the 3-SAT problem has at least literal that must be true. But in Exactly one 3-SAT problem, we determine if the CNF is satisfiable where exactly one of the three literals in every clause is true and the other two are false. This problem is NP-Complete.
Exactly one 3-SAT is a known NP-Complete problem, and it’s used in reduction to prove other problems NP-complete.
5. Cook-Levin Theorem
In this section, we’ll discuss the Cook-Levin theorem which shows how to prove that the SAT is an NP-Complete problem.
The statement of Cook-Levin theorem is the boolean satisfiability problem is NP-complete.
For a given truth assignment, we can verify if the CNF or boolean expression is satisfiable or not in polynomial time.
If a decision problem can be verified in polynomial time by a deterministic Turing machine, then it can be solved in polynomial time by a non-deterministic algorithm. Proof of this statement can be found in multiple textbooks.
SAT is in NP if there is a non-deterministic Turing machine that can solve it in polynomial time.
If any problem in NP can be reduced to an SAT problem in Polynomial-time, then it’s NP-Complete. We can prove by taking any language and reducing it to SAT in polynomial time. Because , there exists a verifier which can verify the decision problem in polynomial time.
Let be an input on which verifier checks if the output is a yes or a no or ( or ). Because works in polynomial time, at every time step, the algorithm makes the hardware affect a constant number of memory units.
After time steps, the algorithm affects memory units. We can represent each of these operations at every time step using AND, OR, NOT logical gates. Hence it is possible to build a circuit in polynomial for any language . This would be a polynomial time in the number of bits present in input .
The decision problem now reduces to determining if there is an input for which the circuit built above outputs (true). The CNF equivalents of AND, OR, and NOT gates are shown below. This reduction is done using De Morgan’s laws, material implication, and double negation.
Let’s start with AND gate. Let , be the inputs, be the output:
The functionality of the above AND gate in CNF form is:
For OR gate, let , be the inputs, be the output:
The functionality of the above OR gate in CNF form is:
For NOT gate, let be the input, be the output:
The functionality of the above NOT gate in CNF form is:
From the above gates, we can observe that we can convert the circuit into an equivalent CNF form.
Hence all NP-Hard problems can be reduced to CNF, which means, they can be reduced to an SAT problem. Hence the SAT is NP-Complete.
6. Introduction to 3-SAT
3-SAT defines the problem of determining whether a given CNF, with each clause containing at most literals, is satisfiable or not.
The 3-SAT problem is simpler then 2-SAT as it seeks to solve the 2-SAT problem where there can be at most three variables in each parenthesis in the boolean expression. Still, there is no polynomial-time algorithm exists for 3-SAT.
Let’s see an example. We’ll take an SAT problem and make it a 3-SAT.
We’re taking an example of an SAT problem:
is satisfiable for truth values:
, , , , , ,
We can introduce two new variables to make the given SAT problem to a 3-SAT problem:
is satisfiable for truth values , , , , , , , , . In fact, for either values of and , the 3-CNF is satisfiable.
7. NP-Completeness of 3-SAT
In this section, let’s see how we can prove that 3-SAT is NP-Complete.
We can convert any problem into an SAT problem in polynomial time. That is, we can express it as a boolean formula and can convert every boolean formula into its corresponding CNF form.
SAT to 3-SAT reduction takes polynomial time. That is the corresponding CNF to 3-CNF takes polynomial time. Let the CNF representation of the original SAT problem is:
where is satisfiable if every clause is satisfiable.
Without loss of generality, let’s assume that the clause has more than literals:
where each is picked from a set of literals:
Let
Define as following:
where is a new variable and we introduce it to make a clause with literals. This same procedure can be applied repeatedly to the second clause in until there are no more clauses with more than three literals remaining.
Now we need to prove that and are equisatisfiable.
For case 1 we need to show is satisfiable, then is satisfiable. Let’s start this proof:
is satisfiable, then is satisfiable
if
(1)
if
(2)
For either values of , for to be satisfiable, either or . From (1) and (2), we can say that if .
If satisfiable, then is satisfiable.
If either or , then we can assign and because:
and one or both of are .
If , then . By assigning , we can make satisfiable.
Using the above procedure, where the number of literals is greater than can be converted into clauses with at most variables that are equisatisfiable. From the above proof, we can see that this takes polynomial time in the number of literals in every clause.
Therefore, we can reduce the SAT to 3-SAT in polynomial time. From Cook’s theorem, the SAT is NP-Complete. Hence 3-SAT is also NP-Complete.
8. Conclusion
In this tutorial, we’ve presented a detailed discussion of the SAT problem. We’ve discussed the Cook-Levin theorem to show SAT is an NP-Complete problem.
Furthermore, we’ve given a short introduction to the 3-SAT problem and showed a reduction of SAT to 3-SAT.