A Full Step-by-Step CDCL Example
Here’s a complete CDCL run, with decision levels, unit propagation, a conflict,
1-UIP-style resolution to a learned clause, and a backjump, ending with a satisfying
assignment.
The CNF instance
Variables: A, B, C, D, E (and I’ll also use a “dummy” decision P just to show backjumping past
an irrelevant decision).
Clauses:
1. (A ∨ B)
2. (¬A ∨ C)
3. (¬B ∨ C)
4. (¬C ∨ D)
5. (¬C ∨ E)
6. (¬D ∨ ¬E)
Intuition: if C becomes true, it forces D and E true, but clause 6 says D and E can’t both
be true → potential conflict.
CDCL run, step by step
Decision level 0
No unit clauses initially, so nothing forced.
Decision level 1: make a decision
Decide: A = False (DL=1)
Now do unit propagation (forced moves):
• Clause 1: (A ∨ B) with A = F becomes (B)
imply B = True (DL=1), reason: clause 1
• Clause 3: (¬B ∨ C) with B = T becomes (C)
imply C = True (DL=1), reason: clause 3
• Clause 4: (¬C ∨ D) with C = T becomes (D)
imply D = True (DL=1), reason: clause 4
• Clause 5: (¬C ∨ E) with C = T becomes (E)
imply E = True (DL=1), reason: clause 5
1
Now check clause 6: (¬D ∨ ¬E). With D = T and E = T , it becomes (F ∨ F ) →
CONFLICT.
At this moment we have an “implication chain”:
A = F ⇒ B = T ⇒ C = T ⇒ D = T and C = T ⇒ E = T , and then conflict on clause 6.
(Optional) show an irrelevant decision level to motivate backjumping
Suppose the solver (in another run ordering) had also made a pointless extra decision before
noticing conflict, e.g.
Decide: P = True (DL=2) — not connected to any clause above.
The conflict analysis will ignore P , and the solver will “jump over” DL=2. (This is the
point of non-chronological backtracking.)
Conflict analysis → clause learning (resolution steps)
Start from the conflicting clause:
• Conflict clause: (¬D ∨ ¬E)
We will resolve away implied literals using their reason clauses until we get a clause that
blocks the “real cause”.
1) Resolve out D
D was implied by clause 4: (¬C ∨ D)
Resolve:
• (¬D ∨ ¬E)
• (¬C ∨ D)
Result:
• (¬C ∨ ¬E)
2) Resolve out E
E was implied by clause 5: (¬C ∨ E)
Resolve:
• (¬C ∨ ¬E)
• (¬C ∨ E)
Result:
• (¬C)
3) Resolve out C
C was implied by clause 3: (¬B ∨ C)
Resolve:
• (¬C)
• (¬B ∨ C)
Result:
• (¬B)
2
4) Resolve out B
B was implied by clause 1: (A ∨ B)
Resolve:
• (¬B)
• (A ∨ B)
Result (learned clause):
• (A)
Learned clause: (A)
Meaning: To avoid this conflict pattern, A must be true. This exactly blocks the bad branch
“A = False” that triggered the cascade.
Backjump + propagate the learned clause
The learned clause (A) is unit.
• The solver backjumps to the highest level where the learned clause becomes unit.
Here, (A) has no other literals, so it becomes unit at decision level 0.
So we:
1. Undo assignments from DL=1 (and also DL=2 like the irrelevant P , if it existed)
2. At DL=0, propagate the learned clause:
• A = True (DL=0), reason: learned clause (A)
This is the “CDCL magic”: we didn’t just flip the last decision; we learned and jumped
to the right place.
Continue search to find a model
Now at DL=0:
• A=T
No forced moves from clauses 2–6 yet.
Decision level 1
Decide: B = False (DL=1)
Propagate:
• Clause 1 (A ∨ B) is already satisfied since A = T .
• Clause 3 (¬B ∨ C) with B = F : ¬B = T → satisfied, no force.
• Clause 2 (¬A ∨ C) with A = T becomes (C)?? Careful: ¬A is false, so it becomes (C).
imply C = True (DL=1), reason: clause 2
Then:
• Clause 4 with C = T D = T
3
• Clause 5 with C = T E = T
• Clause 6 conflicts again (same pattern)
So with A = T , choosing B = F forces C = T via clause 2 and causes conflict. That’s
fine—CDCL would learn again. But we can also avoid it by choosing C = F before it’s forced. . .
except clause 2 forces C when A = T . So instead choose B = T maybe?
Let’s try a different decision:
Backtrack within DL=1 choice: set B = True.
With A = T, B = T :
• Clause 3 (¬B ∨ C) forces C = T (since ¬B is false)
Then again D = T, E = T → conflict.
So whenever A = T , B either way seems to force C = T (via clause 2 if A = T , and via
clause 3 if B = T ). That suggests: to satisfy clause 6, we must prevent C = T , but the system
keeps forcing it. . . so maybe the formula is UNSAT?
Let’s double-check carefully: clause 2 is (¬A ∨ C). If A = T , yes it forces C = T . So any
model with A = T must have C = T . Then C = T forces D = T and E = T , which violates
clause 6. Therefore no model with A = T exists.
But we learned (A) from the earlier conflict—how can that be, if A = T is impossible?
Answer: that means the conflict analysis we did as written can’t be correct unless the
original formula already implies A (which would then make it UNSAT), or we made a
wrong clause choice. And we did: the clause that forced B from (A ∨ B) with A = F is fine,
but the chain that forced C used clause 3 (¬B ∨ C) with B = T , also fine. The resolution steps
are mechanically correct. So the only consistent conclusion is:
With these exact clauses, the formula is actually UNSAT, and learning (A) is part
of proving that.
A SAT-ending version (one-clause tweak)
Replace clause 2 with:
• 2’. (¬A ∨ ¬C)
Now the earlier conflict chain still works when A = F (because clause 2’ is satisfied when
A = F ), but when A = T it forces C = F , which prevents the D/E conflict.
Re-run the key parts after learning (A):
• DL=0: learned clause A = T
• Clause 2’ with A = T becomes (¬C) C = F
• With C = F , clauses 4 and 5 are satisfied (since ¬C is true), so D, E are free.
• Choose D = F, E = F (or anything not violating clause 6), and pick B to satisfy clause
1 (already satisfied because A = T ).
Example satisfying assignment:
• A = T, C = F, B = F, D = F, E = F
All clauses check out with the tweaked clause 2’.
If you want, I can give a clean SAT-ending CDCL trace (no midstream correction) with
a standard textbook CNF that demonstrates:
4
• conflict at DL=3,
• non-chronological backjump to DL=1, and
• a learned clause that is not unit (more realistic).