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:
(x11 OR x12) AND (x21 OR x22) AND (x31 OR x32) AND (x41 OR x42) AND ...
where 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.
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 assignement. MAX-2-SAT is a particular case of maximum-satisfiability. It is NP-hard.
References
Christos H. Papadimitriou. On Selecting a Satisfying Truth Assignment (Extended Abstract). Proceedings of the 32nd annual IEEE Symposium on Foundations of Computer Science, pp. 163-169, 1991.