Satisfiability Problem · Polynomially Solvable Special Cases

Lesson 5

Nikolai Chukhin · Alexander S. Kulikov

A Horn clause is a clause that contains at most one positive literal and an arbitrary number of negative literals. In the Horn-SAT problem, one is given a formula consisting solely of Horn clauses, and the objective is to determine an assignment that sets the minimum number of variables to \(\texttt{True}\) in order to satisfy all clauses.

Theorem. The Horn-SAT problem can be solved in linear time with respect to the size of the input formula.

Proof. Write every Horn clause in the form \[(x_{1}\land\dotsb\land x_{k})\Rightarrow y\] if it has the positive literal \(y\), and as \((x_{1}\land\dotsb\land x_{k})\Rightarrow 0\) if it has no positive literal. Initially, all variables are set to \(\texttt{False}\). Whenever all variables in the antecedent of a clause have become \(\texttt{True}\), the clause forces its positive literal to become \(\texttt{True}\); if the clause has no positive literal, the formula is unsatisfiable. We continue until no new variable is forced. The resulting assignment satisfies all clauses and is contained in every satisfying assignment, so it has the minimum possible number of variables set to \(\texttt{True}\).

To implement this in linear time, remove clauses containing both a variable and its negation. For every remaining clause, maintain the number of antecedent variables that are still \(\texttt{False}\). When a variable becomes \(\texttt{True}\), decrement this counter in every clause containing its negative literal. Each literal is processed only once, so the total running time is linear in the size of the formula.◼

For the curious 🤓

Horn clauses form the fundamental basis of logic programming languages such as Prolog and Datalog. When expressed as an implication, a clause with exactly one positive literal takes the form: \[(P_{1} \land P_{2} \land \dotsb \land P_{n}) \to Q.\] This structure corresponds directly to rules in logic programming, where \(Q\) represents the conclusion that can be inferred if all preconditions \(P_{1}, \dotsc, P_{n}\) hold.

Perhaps surprisingly, if one extends Horn-SAT by allowing quantifiers \(\forall, \exists\) the resulting problem remains solvable in polynomial time (the same also holds for \(2\)-SAT). In contrast, permitting such quantifiers in arbitrary CNF formulas significantly increases the complexity: the problem then becomes PSPACE-complete, whereas the standard SAT problem belongs to NP.

Given that both \(2\)-SAT and Horn-SAT admit linear-time algorithms, one might think that they are similar. However, it is known that \(2\)-SAT is NL-complete (i.e., solvable in nondeterministic logarithmic space). In contrast, Horn-SAT is P-complete. Finally, if one allows both Horn clauses and arbitrary binary clauses (i.e., clauses containing exactly two literals) in a single formula, the problem becomes as hard as general SAT. This hybrid problem is referred to as Mixed Horn-SAT.