TAOCP 7.2.2.2 Exercise 254

Section 7.2.2.2: Satisfiability

Exercise 254. [16] Given the binary clauses ${12, 13, 23, 24, 34}$, what clause will a CDCL solver learn first if it begins by deciding that 1 is true?

Verified: no
Solve time: 1m42s

Solution

The clause set is

$$ F={12,13,23,24,34}. $$

A decision that $1$ is true assigns the literal $1$ to the current decision level. The two clauses containing $1$,

$$ 12,\qquad 13, $$

are immediately satisfied. The remaining clauses are

$$ 23,\qquad 24,\qquad 34. $$

Each of these clauses still contains two unassigned literals, so none is unit. Therefore unit propagation produces no additional assignments.

A CDCL solver learns a clause only after a conflict occurs. No clause in $F$ is falsified by the current assignment, because every remaining clause contains unassigned literals. Hence the solver has not reached a conflict after the decision $1$.

For example, extending the assignment by setting

$$ 2=1,\qquad 3=1,\qquad 4=0 $$

satisfies all clauses, since

$$ 12,\quad 13,\quad 23 $$

are satisfied by literals $1$, $2$, or $3$, and

$$ 24,\quad 34 $$

are satisfied by literals $2$ and $3$. Thus the decision $1$ does not lead to an unavoidable contradiction.

Therefore no learned clause is produced at this stage. The first learned clause cannot be determined from the given decision alone, because a conflict requires further decisions.

$$ \boxed{\text{No clause is learned first after only deciding that }1\text{ is true}.} $$