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\_\{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 implication graphs, 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.

Contents

References

References

★ A linear-time algorithm for testing the truth of certain quantified boolean formulas, Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E., , , Information Processing Letters, 1979

★ Computational Complexity, Papadimitriou, Christos H., , , Addison-Wesley, 1994, ISBN 0-201-53082-1

★ Approximation Algorithms, Vazirani, Vijay V., , , Springer-Verlag, 2003, ISBN 3-540-65367-8