2-satisfiability

Encyclopedia : 2 : 2S : 2SA : 2-satisfiability

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_ \lor x_) \land (x_ \lor x_) \land \cdots \land (x_ \lor x_) \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-complete.

References

Christos H. Papadimitriou. Computational Complexity (chapter 4.2). Addison-Wesley, 1994. ISBN 0-201-53082-1

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.