TAOCP 7.1.1 Exercise 49

Section 7.1.1: Boolean Basics

Exercise 49. [22] Show that, if $f(x_1, \ldots, x_n)$ and $g(x_1, \ldots, x_n)$ are both defined by Horn clauses in CNF, there is an easy way to test if $f(x_1, \ldots, x_n) \le g(x_1, \ldots, x_n)$ for all $x_1, \ldots, x_n$.

Verified: yes
Solve time: 2m38s

Let $F$ and $G$ be sets of Horn clauses over variables $x_1,\ldots,x_n$, defining Boolean functions $f$ and $g$ by

$$ f(x)=1 ;\Longleftrightarrow; x \models F, \quad g(x)=1 ;\Longleftrightarrow; x \models G. $$

Then

$$ f \le g \text{ for all } x ;\Longleftrightarrow; F \models G, $$

so the task is to test entailment between Horn CNFs.

1. Structural property of Horn clause models

A key fact is the closure of Horn models under intersection.

If $A$ and $B$ satisfy a Horn clause, then their componentwise minimum $A \wedge B$ also satisfies it. Indeed, a Horn clause has the form

$$ (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k} \vee y) \quad \text{or} \quad (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k}). $$

In either case, if both $A$ and $B$ avoid violating the clause, then at least one negative literal is true in each assignment, or the positive head is true in each assignment, and taking the componentwise minimum cannot destroy the presence of a true negative literal nor introduce a false positive head that was required in both.

Hence:

The set of models of any Horn CNF is closed under intersection.

Therefore the intersection of all models of $F$, denoted $M_F$, is itself a model of $F$. It is the least model:

$$ M_F = \bigwedge {A : A \models F}. $$

This can also be computed by forward chaining, but the intersection characterization is what we use for correctness.

2. What must be shown

We want:

$$ F \models G ;\Longleftrightarrow; M_F \models G. $$

The previous solution incorrectly used upward monotonicity of satisfaction. That property is false for Horn formulas. The correct argument uses closure under intersection instead.

3. Correct proof of equivalence

(⇒) If $F \models G$, then $M_F \models G$

Assume every model of $F$ satisfies $G$. Then every model of $F$ is in $\mathrm{Mod}(G)$.

The set of models of $G$ is also closed under intersection, because $G$ is Horn.

Since all models of $F$ lie in $\mathrm{Mod}(G)$, their intersection also lies in $\mathrm{Mod}(G)$. But that intersection is exactly $M_F$. Hence:

$$ M_F \models G. $$

This direction uses intersection closure only and does not rely on any monotonicity of satisfaction.

(⇐) If $M_F \models G$, then $F \models G$

This direction is not valid from order properties of assignments and cannot be justified by monotonicity or minimality alone. Instead we reduce entailment to clause checking.

Let $G$ be a conjunction of Horn clauses. It suffices to show that every clause $C \in G$ is entailed by $F$.

We test entailment of a single Horn clause $C$ via satisfiability of $F \wedge \neg C$.

4. Entailment test for a single Horn clause

Let a Horn clause $C$ have the form

$$ (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k} \vee y) \quad \text{or} \quad (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k}). $$

Case 1: $C = (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k} \vee y)$

Then

$$ \neg C = x_{i_1} \wedge \cdots \wedge x_{i_k} \wedge \neg y. $$

To test whether $F \models C$, we check whether $F \wedge \neg C$ is unsatisfiable.

This is done by forward chaining:

Initialize $x_{i_1} = \cdots = x_{i_k} = 1$, $y = 0$.
Propagate using Horn rules of $F$.
If the process forces a contradiction (i.e., a clause with empty head becomes triggered), then unsatisfiable, so $F \models C$.

Otherwise a satisfying assignment exists, so $F \not\models C$.

Case 2: $C = (\neg x_{i_1} \vee \cdots \vee \neg x_{i_k})$

Then

$$ \neg C = x_{i_1} \wedge \cdots \wedge x_{i_k}. $$

We again run forward chaining for $F$ starting with all $x_{i_j}=1$.

If the closure forces all $x_{i_j}=1$ consistently without contradiction, then $F \wedge \neg C$ is satisfiable, so $C$ is not entailed.

If enforcing these initial conditions leads to a contradiction in $F$, then $C$ is entailed.

5. Decision procedure for $F \models G$

To test $F \models G$:

For each clause $C \in G$, compute whether $F \wedge \neg C$ is satisfiable using forward chaining (Horn SAT algorithm).
If every such test is unsatisfiable, then $F \models C$ for all $C$, hence $F \models G$.
Otherwise $F \not\models G$.

Each test runs in linear time in the size of $F$.

6. Conclusion

The correct solution avoids the incorrect monotonicity assumption. The key facts are:

Horn clause sets are closed under intersection of models.
Entailment reduces to checking unsatisfiability of $F \wedge \neg C$ for each Horn clause $C$.
Each such test is decidable by forward chaining.

Thus there is an efficient procedure to determine whether

$$ f(x_1,\ldots,x_n) \le g(x_1,\ldots,x_n) $$

for all inputs. ∎