TAOCP 7.2.2.2 Exercise 386

Let $C$ be a clause in $\Phi$, and suppose that $C$ contains a literal $l$ such that $C\circ C'$ is certifiable for $\Phi\setminus C$ whenever $C'\in\Phi$ contains $\bar l$.

taocpmathematicsalgorithmsvolume-4math-medium

Section 7.2.2.2: Satisfiability

Exercise 386. ▶ [M25] Let Algorithm $C_0$ be a variant of Algorithm $C$ that (i) makes all decisions at random; (ii) never forgets a learned clause; and (iii) restarts whenever a new clause has been learned. (Thus, step C5 ignores $M_0$ and $M_1$; step C6 chooses $l$ uniformly at random from among the $2(n-F)$ currently unassigned literals; step C8 backjumps while $F > t_1$, instead of while $F > t_{d'-1}$; and after step C9 has stored a new clause, with $d > 0$, it simply sets $d \leftarrow 0$ and returns to C2. The data structures HEAP, OVAL, and ACT are no longer used.) We will prove that Algorithm $C_0$ is, nevertheless, quite powerful.

In the remainder of this exercise, $F$ denotes the set of clauses known by Algorithm $C_0$, both original and learned; in particular, the unit clauses of $F$ will be the first literals $L_0, L_1, \ldots, L_{t_1-1}$ on the trail. If $C$ is any clause and if $l \in C$, we define

$$\text{score}(F, C, l) = \begin{cases} \infty, & \text{if } F \wedge \overline{C \setminus l} \vdash l; \ |{l' \mid F \wedge \overline{C \setminus l} \vdash l'}|, & \text{otherwise.} \end{cases}$$

Thus $\text{score}(F, C, l)$ represents the total number of literals on the trail after making all the unforced decisions of $\overline{C \setminus l}$, if no conflict arises. We say that Algorithm $C_0$ performs a "helpful round" for $C$ and $l$ if (i) every decision literal belongs to $\bar{C}$; and (ii) $l$ is chosen as a decision literal only if the other elements of $\bar{C}$ are already in the trail.

  • a) Let $C$ be certifiable for $F$, and suppose that $\text{score}(F, C, l) < \infty$ for some $l \in C$. Prove that if $F'$ denotes $F$ together with a clause learned on a helpful round, then $\text{score}(F', C, l) > \text{score}(F, C, l)$.
  • b) Furthermore $\text{score}(F', C, l) \ge \text{score}(F, C, l) + 1$ after an unhelpful round.
  • c) Therefore $C$ will be absorbed by the set $F'$ of known clauses after at most $|C|n$ helpful rounds have occurred.
  • d) If $|C| = k$, show that $\Pr(\text{helpful round}) \ge (k-1)!/(2n)^k \ge 1/(4n^k)$.
  • e) Consequently, by exercise 385(c), if there exists a certificate of unsatisfiability $(C_1, \ldots, C_q)$ for a family of clauses $F$ with $n$ variables, Algorithm $C_0$ will prove $F$ unsatisfiable after learning an average of $\mu \le 4 \sum_{i=1}^{q} |C_i| n^{1+|C_i|}$ clauses. (And it will q.s. need to learn at most $\mu \ln n \ln \ln n$ clauses, by exercise 308–102.)

Verified: no
Solve time: 5m48s

Solution

Let $C$ be a clause in $\Phi$, and suppose that $C$ contains a literal $l$ such that $C\circ C'$ is certifiable for $\Phi\setminus C$ whenever $C'\in\Phi$ contains $\bar l$. We prove that $C$ may be forgotten.

By the definition of certifiability used in the preceding exercise, every solution of $\Phi\setminus C$ also satisfies every clause $C\circ C'$ that is certifiable for $\Phi\setminus C$. Therefore, if an assignment satisfies $\Phi\setminus C$, it satisfies all clauses of the form $C\circ C'$ for which $C'\in\Phi$ contains $\bar l$.

Consider such an assignment, and suppose that $C$ is false under it. Write

$$ C={l}\cup D, $$

where $D$ contains the remaining literals of $C$. Since $C$ is false, $l$ is false and every literal in $D$ is false.

The assignment can be changed by applying the erp rule

$$ l\leftarrow 1. $$

After this replacement, $C$ is satisfied. It remains to prove that no clause of $\Phi\setminus C$ becomes false.

Only clauses containing $\bar l$ can be affected by this replacement. Let $C'\in\Phi$ contain $\bar l$. Before the replacement, $C'$ was satisfied because the assignment satisfied $\Phi\setminus C$. Assume that after the replacement $C'$ becomes false. Then every literal of $C'$ other than $\bar l$ is false, because $\bar l$ itself is false after $l\leftarrow1$.

The resolvent-like clause $C\circ C'$ consists of the literals of $C$ other than $l$ together with the literals of $C'$ other than $\bar l$. Under the original assignment, every literal in $D$ was false, and under the new assignment every literal of $C'$ other than $\bar l$ is false. Hence $C\circ C'$ would be false after the replacement. Since the replacement changed only the value of $l$, and $l$ does not occur in $C\circ C'$, the original assignment also made $C\circ C'$ false.

This contradicts the fact that every solution of $\Phi\setminus C$ satisfies $C\circ C'$. Therefore no clause $C'$ containing $\bar l$ can be falsified by the replacement.

If a solution of $\Phi\setminus C$ already satisfies $C$, the replacement is unnecessary. If it does not satisfy $C$, the rule $l\leftarrow1$ produces a solution satisfying $C$ while preserving every clause in $\Phi\setminus C$. Hence every solution of $\Phi\setminus C$ can be converted into a solution of $\Phi$.

The reverse implication is immediate because $\Phi$ contains all clauses of $\Phi\setminus C$. Therefore

$$ \Phi\text{ is satisfiable}\iff\Phi\setminus C\text{ is satisfiable}. $$

Thus $C$ may be safely forgotten, and the appropriate erp rule is

$$ \boxed{l\leftarrow1}. $$

This completes the proof. ∎