Module hornsat 

Horn-SAT in linear time via unit propagation (forward chaining).

A Horn clause has at most one positive literal, so it reads as a definite implication (body₁ ∧ … ∧ bodyₖ) → head (or, with no positive literal, a goal (body₁ ∧ …) → false). Such a system has a unique least model, computed by O(n+m) forward chaining: start all-false and fire each implication whose body is fully established. The system is satisfiable iff the least model violates no goal clause. Both verdicts are certified — the least model is re-checkable, and an unsatisfiable system yields the derivation (the clauses that force a goal’s body true) which is_refutation replays independently.

Structs

HornClause

A Horn clause (body ⇒ head): the conjunction of the body variables implies head, or — when head is None — implies false (a goal/integrity clause).

Enums

HornOutcome

The outcome of solving a Horn system.

Functions

is_refutation

Re-check a refutation: replaying only the listed clauses by forward chaining forces some goal clause’s body fully true (a contradiction). A solver-free certificate of unsatisfiability.

satisfies

Re-check a satisfying model: every clause holds (a rule with a true body has a true head; a goal has a false body).

solve

Solve a Horn system over 0..num_vars by forward chaining. Returns the least model, or — if a goal clause is forced — a certified derivation. Linear in the total clause size.