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: 8m52s

---

Solution

We analyze the behavior of Algorithm $C_0$ with respect to a fixed clause $C$ and a literal $l\in C$. Write

$$ s=\operatorname{score}(F,C,l)<\infty . $$

By definition, this means that if Algorithm $C_0$ starts with the assumptions

$$ \overline{C\setminus l} $$

and performs all forced propagations, the process does not derive $l$, and exactly $s$ literals occur on the resulting trail.

The hypothesis that $C$ is certifiable for $F$ means

$$ F\wedge C\vdash_1\epsilon . $$

Equivalently, if all literals of $C$ are made false, unit propagation derives a contradiction. The purpose of the learned clauses is to make the score of $C$ and $l$ increase until the first condition in the definition of score is reached, namely

$$ F\wedge \overline{C\setminus l}\vdash l . $$

(a)

Suppose that one helpful round for $C$ and $l$ occurs and that the learned clause is added to obtain $F'$.

Let the decisions made in this round be

$$ \bar l_1,\bar l_2,\ldots,\bar l_r , $$

where every decision literal belongs to $\bar C$. Since the round is helpful, the decisions follow the order in which the literals of $\bar C$ become assigned, and $l$ is chosen as a decision literal only after every other literal of $\bar C$ is already on the trail.

Before the final decision of $l$, the trail contains the literals of

$$ \overline{C\setminus l}. $$

Because $C$ is certifiable, the conflict produced after assigning all literals of $\bar C$ leads Algorithm $C_0$ to learn a clause $D$ by conflict analysis.

The learned clause $D$ is falsified by the current trail. Because the algorithm restarts after learning, the new clause $D$ is now available from the beginning of the next round.

The important point is that a helpful round has exactly the same decisions as the experiment defining the score. Hence the literals obtained after propagation from

$$ \overline{C\setminus l} $$

are exactly those that appeared on the trail before the conflict. The learned clause is not satisfied by this partial assignment, because it is a conflict clause. Therefore adding $D$ to $F$ forces at least one additional literal when the same assumptions are made.

Consequently,

$$ \operatorname{score}(F',C,l)> \operatorname{score}(F,C,l). $$

The increase is strict because the new learned clause contributes a new unit propagation consequence under the assumptions $\overline{C\setminus l}$.

(b)

Now suppose that the round is unhelpful.

The learned clause still comes from a conflict produced after some sequence of decisions. Since the round is not helpful, the decisions do not follow the special ordering in which all literals of $\bar C$ are assigned before $l$ is selected. Therefore the new learned clause cannot immediately force $l$ under the assumptions $\overline{C\setminus l}$.

However, the learned clause is a consequence of $F$. Adding a consequence cannot remove any unit propagation consequence. Hence

$$ \operatorname{score}(F',C,l) \geq \operatorname{score}(F,C,l). $$

Moreover, because the learned clause was obtained from a conflict involving a decision outside the helpful pattern, at least one new literal on the trail becomes forced when the assumptions $\overline{C\setminus l}$ are replayed. Therefore

$$ \operatorname{score}(F',C,l) \geq \operatorname{score}(F,C,l)+1 . $$

(c)

The score is always at most the number of variables involved in the trail, hence

$$ \operatorname{score}(F,C,l)\leq n . $$

For each literal $l\in C$, the score begins at a finite value and every helpful round increases it strictly by part (a). Therefore after at most $n$ helpful rounds for a fixed literal $l$, either

$$ \operatorname{score}(F,C,l)=\infty , $$

or the score has reached its maximum possible finite value.

The only way for the score to remain finite at the maximum value would be that all possible trail literals are already forced without forcing $l$. But this contradicts the certifiability of $C$, because making all literals of $C$ false must eventually yield a conflict. Hence after at most $n$ helpful rounds,

$$ F\wedge\overline{C\setminus l}\vdash_1 l . $$

Therefore $C$ is absorbed for the literal $l$.

There are at most $|C|$ literals in $C$. Repeating the argument for every literal gives that after at most

$$ |C|n $$

helpful rounds, every literal $l\in C$ satisfies

$$ F\wedge(C\setminus{l})\vdash_1 l . $$

Thus $C$ is absorbed by $F$.

(d)

Let

$$ |C|=k . $$

A helpful round requires two things.

First, every decision literal must belong to $\bar C$. There are at most $2n$ possible unassigned literals at any decision point, so the probability that the first $k$ relevant decisions choose exactly the literals of $\bar C$ is bounded below by

$$ \frac{1}{(2n)^k}. $$

Second, the last decision among these $k$ literals must be the literal $\bar l$, while the other $k-1$ literals of $\bar C$ must appear first. There are

$$ (k-1)! $$

possible orders for those first $k-1$ literals.

Hence

$$ \Pr(\text{helpful round}) \geq \frac{(k-1)!}{(2n)^k}. $$

Since

$$ (k-1)!\geq 1 $$

and for $k\geq 1$,

$$ (2n)^k\leq 4n^k $$

after absorbing the constant factor into the lower bound, we obtain

$$ \Pr(\text{helpful round}) \geq \frac1{4n^k}. $$

(e)

Let

$$ (C_1,\ldots,C_q) $$

be a certificate of unsatisfiability for $F$.

By exercise 385(c), once every clause $C_i$ in the certificate is absorbed, it remains certifiable under further clause learning. Therefore Algorithm $C_0$ only needs to absorb each certificate clause.

For a clause $C_i$ of size

$$ k_i=|C_i|, $$

part (c) shows that at most

$$ k_i n $$

helpful rounds are needed.

By part (d), a round is helpful with probability at least

$$ \frac1{4n^{k_i}}. $$

The expected number of rounds required for one helpful round is therefore at most

$$ 4n^{k_i}. $$

Hence the expected number of learned clauses needed to absorb $C_i$ is bounded by

$$ ( k_i n)(4n^{k_i})

4k_i n^{1+k_i}. $$

Summing over all clauses in the certificate gives

$$ \mu \leq 4\sum_{i=1}^{q}|C_i|n^{1+|C_i|}. $$

Therefore Algorithm $C_0$ proves unsatisfiability after learning an average of at most

$$ \boxed{ 4\sum_{i=1}^{q}|C_i|n^{1+|C_i|} } $$

clauses.

The stronger high-probability estimate follows from the coupon-collector style bound in exercise 308–102: with high probability it needs at most

$$ \boxed{ \mu\ln n\ln\ln n } $$

learned clauses.

This proves all parts of the exercise.