2-satisfiability

From Wikipedia, the free encyclopedia

You have new messages (last change).

2-satisfiability (abbreviated as 2-SAT) is a special case of satisfiability if expressions are written in conjunctive normal form with 2 variables per clause (2-CNF). This means the expression has the form:

(x_{11} \lor x_{12}) \land (x_{21} \lor x_{22}) \land \cdots \land (x_{n1} \lor x_{n2}) \land \cdots

where \lor means OR, \land means AND, each x is a variable, with or without a NOT in front of it, and each variable can appear multiple times in the expression.

Unlike general satisfiability or 3-satisfiability which are NP-complete and have no known efficient algorithm, 2-satisfiability can be solved in polynomial time. There are several known polynomial time algorithms for 2-SAT, for example, based on resolution or random walks. More powerfully, 2-satisfiability is NL-complete (Papadimitriou 1994, Thrm. 16.3), meaning that it is one of the "hardest" or "most expressive" problems which can be solved in nondeterministic logspace (NL).

A related problem is maximum-2-satisfiability (MAX-2-SAT) in which the input is still a 2-CNF but we have to determine the maximum number of clauses that can be simultaneously satisfied by an assignment. MAX-2-SAT is a particular case of maximum-satisfiability. It is NP-Hard.

[edit] References

  • Christos H. Papadimitriou. Computational Complexity (chapter 4.2). Addison-Wesley, 1994. ISBN 0-201-53082-1
  • Vijay V. Vazirani. Approximation Algorithms (chapter 16). Springer, 2003. ISBN 3-540-65367-8Template:Cs-stub
Retrieved from "http://en.wikipedia.org../../../2/-/s/2-satisfiability.html"