3-SAT Task

From GM-RKB
Jump to navigation Jump to search

A 3-SAT Task is a Boolean Satisfiability Task that involves conjunction of 3-clause disjunctions.



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

      "(l1l2x2) ∧

      x2 ∨ l3x3) ∧

      x3 ∨ l4x4) ∧ … ∧

      xn-3ln-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 ∨ … ∨ ljdj+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.

  1. i.e. at least as hard as every other problem in NP. A problem is NP-complete if and only if it is in NP and is NP-hard.
  2. i.e. such that one literal isn't the negation of the other
  3. viz. all maxterms that can be built with d1,...,dk, except "d1∨...∨dk