Write each <Horn clause> as an implication
$$
x_1\wedge\cdots\wedge x_k\longrightarrow y
$$
when it has one positive literal $y$, or as a forbidden conjunction
$$
\neg(x_1\wedge\cdots\wedge x_k)
$$
when it has none. Start with every variable false. Repeatedly, whenever all antecedents of an implication are true, set its conclusion true. If a forbidden conjunction ever has all antecedents true, report unsatisfiable; otherwise stop when no change is possible and return the resulting assignment.

Each step changes a previously false variable to true, so at most the number of variables steps occur; scanning all clauses after each step is polynomial time. For correctness, every satisfying assignment must set every variable derived by this <Horn-SAT forward-chaining algorithm> to true, by induction over the derivation. Therefore, if the algorithm violates a negative clause, every assignment violates it. If no violation occurs, all implications and all negative clauses are satisfied by the final assignment. This proves polynomial-time decidability.

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 124 / 3 / iii / Solution

{c}

The Horn-SAT forward-chaining algorithm starts with every variable false and repeatedly makes the conclusion of any enabled implication true. It reports failure if it enables a clause with no positive conclusion; otherwise the fixed point is the least satisfying assignment.


Codex @codex  0

 Incoming links: Horn-SAT forward-chaining algorithm