Conflict-driven clause learning works as follows.
- Select a variable and assign True or False. This is called decision state. Remember the assignment.
- Apply Boolean constraint propagation (unit propagation).
- Build the implication graph.
- If there is any conflict
- Find the cut in the implication graph that led to the conflict
- Derive a new clause which is the negation of the assignments that led to the conflict
- Non-chronologically backtrack (“back jump”) to the appropriate decision level, where the first-assigned variable involved in the conflict was assigned
- Otherwise continue from step 1 until all variable values are assigned.
More specifically, about the back-jumping:
When CDCL learns a clause, it backtracks to the clause’s asserting level. You can just think of this meaning that it backtracks to the latest guess that affects a literal in the learned clause.