Schaefer showed, long ago, that there are, essentially, only three non-trivial classes of conjunctive Booleanformulae (or constraint satisfaction problems) for which satisability can be decided in polynomial time(assuming P 6= NP ). These three classes are LIN, 2-SAT and HORN-SAT. LIN is the constraintsatisfaction problem in which all the constraints are linear equations modulo 2. 2-SAT is the constraintsatisfaction problem in which all the constraints are disjunctions of at most two...