HornSAT

HornSAT is the decision problem of determining whether a given conjunction of Horn clauses is satisfiable. A Horn clause is a disjunction of literals containing at most one positive literal. Horn clauses can be written in implication form as (x1 ∧ x2 ∧ ... ∧ xk) → y, where y is a single positive literal, or as a constraint with no positive literal, such as (x1 ∧ x2 ∧ ... ∧ xk) → false. A theory composed of Horn clauses is satisfiable if there exists a truth assignment to the variables that makes every clause true.

HornSAT is solvable in polynomial time, and in fact in linear time with respect to the size of the input using a forward-chaining or least-model algorithm. The standard approach computes the least model of the definite Horn clauses. Start by setting all variables to false, and repeatedly apply definite clauses whose premises are all true to deduce their head as true. Facts (clauses with an empty premise) are immediately true. This forward propagation continues until no new truths can be derived. If no constraint clause of the form (¬x1 ∨ ... ∨ ¬xk) becomes false (i.e., all premises x1, ..., xk are true) the obtained assignment satisfies all clauses, and the instance is satisfiable. If such a constraint is forced to be false, the theory is unsatisfiable.

HornSAT is a staple problem in logic programming and automated reasoning, reflecting the tractability of reasoning with definite Horn clauses. It is a subset of CNF-SAT and is related conceptually to other tractable satisfiability problems, such as 2-SAT, while being distinct in its use of Horn clauses.