Lesson 1

In the general case, the satisfiability problem is algorithmically hard. It is unknown whether it can be solved in polynomial time. Nevertheless, there are several special cases of this problem for which efficient algorithms can be constructed. We will consider two such special cases.

• 2-satisfiability:  each clause of the formula contains at most two literals.


• Horn satisfiability:  each clause of the formula contains at most one positive literal.