# 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 “

*l*" to a conjunction ofl_{1}∨ … ∨n_{}*n*-2 clauses"(l

l_{1}∨x_{2}∨_{2}) ∧(¬

*x*_{2}∨ lx_{3}∨_{3}) ∧(¬

*x*_{3}∨ lx_{4}∨_{4}) ∧ … ∧(¬

*x*_{n-3}∨*l*_{n-2}∨ x_{n-2}) ∧(¬x

_{n-2}∨ ln-1 ∨_{}*l*_{n})", where*x*_{2},...,x_{n-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.

^{[1]}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.

^{[note 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*c^{[note 2]}literals from different clauses, cf. picture. The graph has a*-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.^{[2]}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 "*l*_{1}∨ … ∨*l*_{j}" with*j*<*k*literals can be padded with fixed dummy variables to "ll_{1}∨ … ∨j_{}*∨*dj_{}*+1 ∨ … ∨*dk_{}*".**After padding all clauses, 2*k^{}*-1 extra clauses*d^{[note 3]}have to be appended to ensure that onlyd_{1}=...=_{k}=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

Cite error: `<ref>`

tags exist for a group named "note", but no corresponding `<references group="note"/>`

tag was found, or a closing `</ref>`

is missing