ABSTRACT
In this chapter we discuss several classes of formulas for which the satisfiability problem can be solved in polynomial time. They include positive formulas, negative formulas, CNF formulas consisting of Horn clauses, CNF formulas consisting of dual Horn clauses, CNF formulas built of of 2-clauses, formulas expressed as collections of linear expressions over the field Z2 (affine formulas), and DNF formulas. The polynomial time algorithms for these classes vary in difficulty, and some of these cases are very easy.
