TAOCP 7.1.1 Exercise 42

Section 7.1.1: Boolean Basics

Exercise 42. [20] Find a short, unsatisfiable CNF that is not totally trivial, although it consists entirely of Horn clauses that are also Krom clauses.

Verified: yes
Solve time: 1m01s

Solution

Let the Boolean variables be $x, y$.

Consider the conjunctive normal form

$$ F ;=; x ;\wedge; (\bar{x} \vee y) ;\wedge; (\bar{y} \vee x) ;\wedge; (\bar{x} \vee \bar{y}). $$

Each clause has at most one positive literal, so each clause is a Horn clause. Each clause has at most two literals, so each clause is a Krom clause.

The first clause is the unit clause $x$. The second clause $(\bar{x} \vee y)$ contains one positive literal $y$. The third clause $(\bar{y} \vee x)$ contains one positive literal $x$. The fourth clause $(\bar{x} \vee \bar{y})$ contains no positive literals. Hence all clauses satisfy the Horn condition, and each contains at most two literals, hence satisfies the Krom condition.

Assume an assignment satisfies $F$. The unit clause forces $x = 1$. Substituting into $(\bar{x} \vee y)$ gives $y = 1$. Substituting $x = 1$ and $y = 1$ into $(\bar{x} \vee \bar{y})$ yields $0 \vee 0 = 0$, contradicting satisfiability. Hence no assignment satisfies $F$.

Conversely, no assignment exists, so $F$ is unsatisfiable.

This completes the proof. ∎