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.