3-SAT Task
A 3-SAT Task is a Boolean Satisfiability Task that involves conjunction of 3-clause disjunctions.
- AKA: 3-Satisfiability.
- …
- Counter-Example(s):
- a 2-SAT Task.
- a 3-Coloring Task.
- See: Equisatisfiable, NP-Complete Problem, NP-Hard, Polynomial-Time Reduction, Clique Problem, Graph (Mathematics), Exponential Time Hypothesis.
References
2014
- (Wikipedia, 2014) ⇒ http://en.wikipedia.org/wiki/boolean_satisfiability_problem#3-satisfiability Retrieved:2014-7-26.
- Like the satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called 3-SAT, 3CNFSAT, or 3-satisfiability.
To reduce the unrestricted SAT problem to 3-SAT, transform each clause “l1 ∨ … ∨ ln" to a conjunction of n-2 clauses
"(l1 ∨ l2 ∨ x2) ∧
(¬x2 ∨ l3 ∨ x3) ∧
(¬x3 ∨ l4 ∨ x4) ∧ … ∧
(¬xn-3 ∨ ln-2 ∨ xn-2) ∧
(¬xn-2 ∨ ln-1 ∨ ln)", where x2,...,xn-2 are fresh variables not occurring elsewhere.
Although both formulas are not logically equivalent, they are equisatisfiable. The formula resulting from transforming all clauses is at most 3 times as long as its original, i.e. the length growth is polynomial.
3-SAT is one of Karp's 21 NP-complete problems, and it is used as a starting point for proving that other problems are also NP-hard.[1] This is done by polynomial-time reduction from 3-SAT to the other problem. An example of a problem where this method has been used is the clique problem: given a CNF formula consisting of c clauses, the corresponding graph consists of a vertex for each literal, and an edge between each two non-contradicting[2] literals from different clauses, cf. picture. The graph has a c-clique if and only if the formula is satisfiable. There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)n where n is the number of clauses and succeeds with high probability to correctly decide 3-SAT.
The exponential time hypothesis is that no algorithm can solve 3-SAT faster than o(exp(n)).
Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3-SAT formulas, depending on their size parameters.
Difficulty is measured in number recursive calls made by a DPLL algorithm. 3-satisfiability can be generalized to k-satisfiability ('k-SAT), when formulas in CNF are considered with each clause containing up to k literals. However, since for any k≥3, this problem can neither be easier than 3-SAT nor harder than SAT, and the latter two are NP-complete, so must be k-SAT. Some authors restrict k-SAT to CNF formulas with exactly k literals. This doesn't lead to a different complexity class either, as each clause "l1 ∨ … ∨ lj" with j<k literals can be padded with fixed dummy variables to "l1 ∨ … ∨ lj ∨ dj+1 ∨ … ∨ dk".
After padding all clauses, 2k-1 extra clauses[3] have to be appended to ensure that only d1=...=dk=FALSE can lead to a satisfying assignment. Since k doesn't depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whether duplicate literals are allowed in clauses (like e.g. "¬x ∨ ¬y ∨ ¬y”), or not.
- Like the satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called 3-SAT, 3CNFSAT, or 3-satisfiability.