3-SAT Task

From GM-RKB
Jump to: navigation, 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.[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[note 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.[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 "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[note 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. ; here: Thm.10.4
  2. Cite error: Invalid <ref> tag; no text was provided for refs named Schoning.1999


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