Horn Formula

logic computation

Definition

Horn Formula

A Horn formula is a conjunction of Horn clauses.

Simplification

Naturally, Horn formulas can be simplified using unit propagation:

Definition

Unit Propagation

Let $S$ be a set of clauses. Unit propagation is the repeated application of the following transformation.

If $S$ contains a unit clause, that is, a clause consisting of a single literal $L$, then:

1. Remove from $S$ every clause of the form $L\vee C$.
2. Replace in $S$ every clause of the form $\neg L\vee C$ by the clause $C$.

The process continues until no unit clause remains. At that point one of three situations holds:

• $S$ is empty: every clause was satisfied, so the original set is satisfiable.
• $S$ contains the empty clause $\square$: a contradiction was derived, so the original set is unsatisfiable.
• $S$ contains non-unit clauses only: no further simplification is possible without choosing a literal to branch on.

Intuitively, $L$ must be true, so every clause containing $L$ is already satisfied and can be discarded, while $\neg L$ is false and can be deleted from every clause that contains it.

Link to original

Tractability

Horn formulas form a sub-class of SAT that is efficiently solvable.