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₁ ∨ … ∨ ln” to a conjunction of n-2 clauses

    "(l₁ ∨ l₂ ∨ x₂) ∧

    (¬x₂ ∨ l₃ ∨ x₃) ∧

    (¬x₃ ∨ l₄ ∨ x₄) ∧ … ∧

    (¬x_n-3 ∨ l_n-2 ∨ x_n-2) ∧

    (¬x_n-2 ∨ ln-1 ∨ l_n)", where x₂,...,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.

    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. 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 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 "l₁ ∨ … ∨ l_j” with j<k literals can be padded with fixed dummy variables to "l₁ ∨ … ∨ lj ∨ dj+1 ∨ … ∨ dk".

    After padding all clauses, 2k-1 extra clauses have to be appended to ensure that only d₁=...=d_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.

---