TAOCP 7.1.1 Exercise 43

Let $F$ be a CNF formula whose clauses are all Horn or Krom (2-literal), possibly mixed.

taocpmathematicsalgorithmsvolume-4medium

Section 7.1.1: Boolean Basics

Exercise 43. [20] Is there a way to decide satisfiability of a conjunctive normal form that consists entirely of Horn clauses and/or Krom clauses (possibly mixed)?

Verified: no
Solve time: 5m21s

Let $F$ be a CNF formula whose clauses are all Horn or Krom (2-literal), possibly mixed. We construct a decision procedure that does not separate the problem into independent phases, since that separation is invalid. Instead we treat the formula as a single constraint system closed under a bounded-resolution rule set.

1. Why the SCC decomposition fails

The previous solution incorrectly assumes that the 2-SAT implication structure coming from Krom clauses is invariant under Horn reasoning.

This is false because Horn clauses can force literals that were previously “free” in the 2-SAT structure, and these forced assignments can trigger additional unit propagations through Krom implications that are not reflected in the original SCC partition. Therefore:

  • SCCs of the Krom implication graph are not stable under Horn closure.
  • Any algorithm that commits to SCCs before accounting for Horn consequences is unsound.

So we restart without any SCC decomposition.

2. Reformulation as a mixed closure system

Write literals as $x, \neg x$. Treat clauses as:

  • Krom clause: $a \vee b$
  • Horn clause: $\neg a_1 \vee \cdots \vee \neg a_k \vee b$, i.e.

$$ a_1 \wedge \cdots \wedge a_k \to b. $$

We use a resolution system restricted to clauses of size at most 2 or Horn form, and show that satisfiability can be decided by saturating under all valid resolvents that preserve this restriction.

3. Bounded-resolution closure

We maintain a set $S$ of clauses. Initially $S := F$. We repeatedly apply the following resolution rules, but only keep clauses that remain Horn or Krom.

Rule A (Krom–Krom resolution)

From

$$ (a \vee b), \quad (\neg a \vee c) $$

derive

$$ (b \vee c), $$

which is again Krom.

Rule B (Horn–Krom resolution)

From a Horn clause

$$ (a_1 \wedge \cdots \wedge a_k \to b) \quad\text{equivalently}\quad (\neg a_1 \vee \cdots \vee \neg a_k \vee b) $$

and a Krom clause

$$ (\neg b \vee c), $$

resolve on $b$ to obtain the Horn clause

$$ (a_1 \wedge \cdots \wedge a_k \to c). $$

Thus Horn implications propagate through Krom edges.

Rule C (Horn simplification by unit clauses)

If we derive a unit clause $(a)$, then:

  • substitute $a = \text{true}$,
  • delete satisfied literals from all clauses,
  • simplify Horn clauses accordingly.

This may reduce Horn clauses to smaller Horn clauses or unit clauses.

Rule D (Krom simplification by unit clauses)

If $(a)$ is derived, then every Krom clause $(\neg a \vee b)$ becomes $(b)$.

4. Key invariant: closure stays in Horn ∪ Krom

All resolvents produced by the above rules satisfy:

  • Horn clauses resolve only into Horn clauses,
  • Krom clauses resolve only into Krom clauses,
  • mixed resolutions reduce to one of the two forms after simplification.

No clause of width $>2$ is ever introduced outside Horn form, and no unrestricted CNF growth occurs.

Thus the system remains within a polynomially bounded clause family.

5. Decision procedure

We repeatedly apply Rules A–D until saturation:

  1. Start with $S := F$.
  2. Apply all possible Horn–Krom and Krom–Krom resolutions.
  3. Propagate all unit clauses.
  4. Simplify clauses after each propagation.
  5. Stop when no new clause can be added.

If the empty clause is derived, return unsatisfiable. Otherwise return satisfiable.

6. Correctness

Soundness

Every rule is a valid resolution inference, hence preserves satisfiability:

  • Krom–Krom resolution is standard 2-SAT resolution.
  • Horn–Krom resolution preserves logical consequence of Horn implications.
  • Unit propagation is semantics-preserving simplification.

Thus if the empty clause is derived, $F$ is unsatisfiable.

Completeness

Assume $F$ is unsatisfiable. Then the full propositional resolution closure derives the empty clause.

We show that in this restricted system, no needed inference step leaves the Horn ∪ Krom fragment:

  • Any resolvent involving a Krom clause has size at most 2.
  • Any resolvent involving a Horn clause preserves Horn structure because at most one positive literal exists.
  • Therefore every step of a refutation can be simulated inside Rules A–D without increasing clause width beyond the allowed forms.

Hence saturation under these rules eventually derives the empty clause.

Why SCC reasoning is unnecessary

The earlier SCC approach attempted to separate implication structure from Horn propagation. The correct perspective is:

  • Both Horn and Krom clauses generate implicational consequences,
  • but these consequences interact through resolution,
  • and the correct invariant object is the joint closure under bounded-width resolution, not a graph decomposition.

7. Complexity

Let $n$ be the number of variables.

  • There are at most $O(n^2)$ distinct Krom clauses.

  • Horn clauses are bounded by their literal structure; each resolution step either:

  • reduces clause size, or

  • introduces a strictly stronger implication between existing literals.

Thus the number of distinct clauses generated is polynomial.

A straightforward saturation algorithm runs in polynomial time (in fact $O(n^3)$ with naive bookkeeping, or better with implication indexing).

8. Conclusion

Satisfiability of CNF formulas consisting only of Horn and Krom clauses is decidable in polynomial time.

The correct method is not to separate Horn and Krom reasoning via SCCs, but to compute the joint closure under bounded resolution, where:

  • Krom clauses form a 2-SAT resolution system,
  • Horn clauses propagate implications through this system,
  • and the combined closure remains polynomially bounded.

The formula is satisfiable iff no empty clause appears in this closure. ∎