TAOCP 7.2.2.2 Exercise 385
We use the following observation about unit propagation.
Section 7.2.2.2: Satisfiability
Exercise 385. [**] Clause $C$ is called certifiable for $F$ if $F \wedge C \vdash_1 c$, as in (119). It is said to be absorbed by $F$ if it is nonempty and $F \wedge C \vdash_1 l$ for every $l \in C$, or if it is empty and $F \vdash_1 \epsilon$. (Every clause of $F$ is obviously absorbed by $F$.)
a) True or false: If $C$ is absorbed by $F$, it is certifiable for $F$.
b) Which of ${1, 12, 123}$ are implied by, certifiable for, or absorbed by $H'$ in (7)?
c) If $C$ is certifiable for $F$ and if all clauses of $F$ are absorbed by $F'$, prove that $C$ is certifiable for $F'$.
d) If $C$ is absorbed by $F$ and if all clauses of $F$ are absorbed by $F'$, prove that $C$ is absorbed by $F'$.
Verified: no
Solve time: 9m20s
Solution
We use the following observation about unit propagation.
If a clause $D$ is absorbed by $G$, then replacing $D$ by $G$ does not weaken unit propagation in any context. Indeed, suppose that under some partial assignment the literals of $D$ except one literal $l$ are false. Since $D$ is absorbed by $G$,
$$ G\wedge (D\setminus{l})\vdash_1 l . $$
Therefore $G$ derives the same unit literal that $D$ would have forced. If $D$ is empty, absorption means that $G\vdash_1\epsilon$.
This observation will be used repeatedly.
(a)
The statement is true.
Assume that $C$ is absorbed by $F$. We prove that
$$ F\wedge C\vdash_1\epsilon . $$
If $C=\epsilon$, then absorption gives immediately
$$ F\vdash_1\epsilon , $$
so $C$ is certifiable.
Now suppose that $C$ is nonempty. Let
$$ C={l_1,\ldots,l_k}. $$
Because $C$ is absorbed by $F$, for every $l_i\in C$,
$$ F\wedge(C\setminus{l_i})\vdash_1 l_i . $$
In particular, after adding all literals of $C$ as unit assumptions, unit propagation can derive every literal of $C$. But those literals are already present as assumptions. More importantly, absorption says that every literal of $C$ is forced by the others. Hence if we negate one literal of $C$, the remaining literals force it, producing a contradiction. Therefore
$$ F\wedge C\vdash_1\epsilon , $$
so $C$ is certifiable for $F$.
Thus every absorbed clause is certifiable.
(b)
This part depends on the definition of the formula $H'$ and the clause set in equation (7), which are not included in the statement. Without the clauses of $H'$, the status of
$$ {1,12,123} $$
cannot be determined.
The required procedure is as follows. For each clause $C\in{1,12,123}$:
- $C$ is implied by $H'$ if every satisfying assignment of $H'$ satisfies $C$.
- $C$ is certifiable for $H'$ if
$$ H'\wedge C\vdash_1\epsilon . $$
- $C$ is absorbed by $H'$ if, for every $l\in C$,
$$ H'\wedge(C\setminus{l})\vdash_1 l , $$
with the empty-clause case handled separately.
The concrete classification requires the missing formula (7).
(c)
Assume that $C$ is certifiable for $F$, and that every clause of $F$ is absorbed by $F'$. We prove that $C$ is certifiable for $F'$.
Since $C$ is certifiable for $F$,
$$ F\wedge C\vdash_1\epsilon . $$
Consider a unit-propagation derivation of the contradiction. Every step that uses a clause of $F$ can be reproduced using $F'$, because every clause $D\in F$ is absorbed by $F'$.
More precisely, suppose a clause $D\in F$ becomes unit during the derivation and forces a literal $l$. Then all literals of $D\setminus{l}$ are false under the current partial assignment. Since $D$ is absorbed by $F'$,
$$ F'\wedge(D\setminus{l})\vdash_1 l . $$
Therefore $F'$ derives the same literal $l$. Every unit step in the derivation from $F\wedge C$ can therefore be reproduced from $F'\wedge C$.
Eventually the same contradiction is reached, giving
$$ F'\wedge C\vdash_1\epsilon . $$
Hence $C$ is certifiable for $F'$.
(d)
Assume that $C$ is absorbed by $F$, and every clause of $F$ is absorbed by $F'$. We prove that $C$ is absorbed by $F'$.
If $C=\epsilon$, absorption of $C$ by $F$ means
$$ F\vdash_1\epsilon . $$
By the argument from part (c), replacing all clauses of $F$ by clauses absorbed by $F'$ preserves this unit contradiction. Hence
$$ F'\vdash_1\epsilon , $$
so $C$ is absorbed by $F'$.
Now suppose $C\neq\epsilon$. Let $l\in C$. Since $C$ is absorbed by $F$,
$$ F\wedge(C\setminus{l})\vdash_1 l . $$
Equivalently,
$$ F\wedge(C\setminus{l})\wedge{\bar l}\vdash_1\epsilon . $$
Thus the clause
$$ {\bar l} $$
is a certifiable contradiction under the assumptions $C\setminus{l}$. By part (c), because every clause of $F$ is absorbed by $F'$, the same certifiability holds with $F'$:
$$ F'\wedge(C\setminus{l})\wedge{\bar l}\vdash_1\epsilon . $$
Therefore unit propagation from
$$ F'\wedge(C\setminus{l}) $$
must derive $l$. Hence
$$ F'\wedge(C\setminus{l})\vdash_1 l . $$
Since this holds for every $l\in C$, the clause $C$ is absorbed by $F'$.
Therefore absorption is preserved when every clause of the original formula is absorbed by the new formula.
∎