Horn-SAT forward-chaining algorithm
= Horn-SAT forward-chaining algorithm
{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.