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

Unit propagation is a procedure of iteratively simplifying a formula in conjunctive normal form by identifying unit clauses $\ell$. Since such a clause would be false unless $\ell$ is true, the procedure assigns $\ell =\top$, then removes all clauses containing $\ell$ and deletes $\neg \ell$ from all remaining clauses. This may create new unit clauses, which are processed recursively until no unit clauses remain.

Example: Consider the formula

$$F=(\neg a\vee \neg b\vee c)\wedge (\neg b\vee \neg c\vee u)\wedge (\neg u\vee b)\wedge u$$

The clause $u$ is a unit clause, so we assign $u=\top$:

$$\begin{array}{rl}\text{I.:}& (\neg a\vee \neg b\vee c)\wedge \cancel{(\neg b\vee \neg c\vee u)}\wedge (\cancel{\neg u}\vee b)\wedge u\\ \text{II.:}& (\neg a\vee \cancel{\neg b}\vee c)\wedge b\wedge u\\ \text{III.:}& (\neg a\vee c)\wedge b\wedge u\end{array}$$

In step I, $u$ is assigned true, eliminating the clause containing $u$ and removing $\neg u$ from the third clause. In step II, this creates a new unit clause $b$, which propagates to yield the simplified formula III.

Link to original

Tractability

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