TAOCP 7.2.2.2 Exercise 206

Section 7.2.2.2: Satisfiability

Exercise 206. [M22] A set of clauses is minimally unsatisfiable if it is unsatisfiable, yet becomes satisfiable if any clause is deleted. Show that, if $F$ and $F'$ have no variables in common, then $F \sqcup F'$ is minimally unsatisfiable if and only if $F$ and $F'$ are minimally unsatisfiable.

Verified: no
Solve time: 1m32s

Solution

Let $H=F\sqcup F'$. The variables introduced by the $\sqcup$ operation will be denoted by $x$, and the clauses inherited from $F$ and $F'$ will be separated according to the side from which they originated. Thus the clauses originating from $F$ have the form $x\cup C$ for clauses $C\in F$, and the clauses originating from $F'$ have the form $\bar{x}\cup C'$ for clauses $C'\in F'$, with the possible replacement of only some clauses allowed by the definition of $\sqcup$.

First suppose that $F$ and $F'$ are both minimally unsatisfiable. Since $F$ and $F'$ are unsatisfiable, the definition of the $\sqcup$ operation gives that $H$ is unsatisfiable. It remains to prove that deleting any clause from $H$ makes it satisfiable.

Let $D$ be a clause of $H$. There are two cases. Suppose first that $D$ is a clause obtained from some $C\in F$. Since $F$ is minimally unsatisfiable, the set $F-{C}$ is satisfiable. Let $L$ be a covering set of strictly distinct literals for $F-{C}$. Also, since $F'$ is minimally unsatisfiable, there is a clause $C'\in F'$ whose deletion gives a satisfiable formula only when that clause is deleted. More generally, because $F'$ itself is satisfiable after deleting any clause, choose any clause $E'\in F'$ and let $L'$ cover $F'-{E'}$. The literals of $F$ and $F'$ are based on disjoint variable sets, so $L\cup L'$ is still a set of strictly distinct literals.

The covering of $H-{D}$ is obtained by choosing the new variable $x$ to have the polarity that satisfies all clauses inherited from $F'$ while preserving the covering of the remaining clauses inherited from $F$. Explicitly, choose $x$ so that every clause $\bar{x}\cup C'$ is covered by $\bar{x}$ if necessary, and choose the literals corresponding to $L$ for the remaining clauses $x\cup C$. The deleted clause $D$ is the only clause whose covering contribution from the $F$ side may fail, and it has been removed. Hence $H-{D}$ is satisfiable.

The same argument applies when $D$ originates from $F'$, with the roles of $F$ and $F'$ interchanged. Therefore every single clause deletion from $H$ produces a satisfiable formula, and $H$ is minimally unsatisfiable.

Now suppose that $H=F\sqcup F'$ is minimally unsatisfiable. Since every clause of $F$ is replaced by a clause containing the new variable $x$, consider the deletion of one such clause $x\cup C$ from $H$. Minimal unsatisfiability implies that the remaining formula is satisfiable. Let $L$ be a satisfying cover of $H-{x\cup C}$. If the value of $x$ is chosen so that $x$ is false, every clause of the form $\bar{x}\cup C'$ is satisfied by $\bar{x}$. Therefore the only conditions imposed on the variables of $F'$ disappear, while the clauses from $F$ that remain reduce to the corresponding clauses of $F$ after removing $x$.

Hence the literals in $L$ restricted to the variables of $F$ cover every clause of $F-{C}$. Since $C\in F$ was arbitrary, every deletion of a clause from $F$ leaves a satisfiable formula.

The same reasoning with $x$ chosen true shows that deleting any clause of $F'$ leaves a satisfiable formula. Thus $F$ and $F'$ are both minimally unsatisfiable, because deleting any clause makes them satisfiable while the original formulas cannot be satisfiable.

Therefore $F\sqcup F'$ is minimally unsatisfiable if and only if $F$ and $F'$ are minimally unsatisfiable.

This completes the proof.

$$ \boxed{\text{$F\sqcup F'$ is minimally unsatisfiable exactly when $F$ and $F'$ are minimally unsatisfiable.}} $$

∎