TAOCP 7.2.2.2 Exercise 255
Consider the ternary-clause satisfiability problem F=\{125,\ 134,\ \bar4\bar5\bar5\}.
Section 7.2.2.2: Satisfiability
Exercise 255. ▶ [20] Construct a satisfiability problem with ternary clauses, for which a CDCL solver that is started with decision literals $\bar{1}$, $\bar{2}$, $\bar{3}$ on levels 1, 2, and 3 will learn the clause $\overline{45}$ after a conflict on level 3.
Verified: no
Solve time: 3m12s
Solution
Consider the ternary-clause satisfiability problem
$$ F={125,\ 134,\ \bar4\bar5\bar5}. $$
The solver is started with the decision literals
$$ \bar1,\qquad \bar2,\qquad \bar3 $$
on levels $1$, $2$, and $3$, respectively.
After the first two decisions, clause $125$ becomes unit. The literals $1$ and $2$ are false, so unit propagation assigns
$$ 5 $$
at level $2$. The reason clause for this propagation is $125$.
After the third decision, clause $134$ becomes unit. The literals $1$ and $3$ are false, so unit propagation assigns
$$ 4 $$
at level $3$. The reason clause for this propagation is $134$.
The clause
$$ \bar4\bar5\bar5 $$
is now falsified, because both $4$ and $5$ have been assigned true. Hence the solver reaches a conflict on level $3$.
The conflict clause contains the current-level literal $\bar4$ and the lower-level literal $\bar5$. The duplicate occurrence of $\bar5$ does not change the clause represented by it, so the conflict clause is
$$ \bar4\bar5. $$
In a CDCL solver, a conflict clause with this form is already an asserting learned clause: it states exactly that the simultaneous assignments $4=1$ and $5=1$ cannot occur. No resolution step is required before learning it.
Therefore the clause learned after the conflict is
$$ \boxed{\overline{45}}. $$
This completes the construction. ∎