Conflict-Driven Clause Learning
Conflict-Driven Clause Learning is a SAT Solver algorithm that improves on DPLL by remembering information across backtracks. It does this reifying both the call stack for backtracking, and the call stack for Unit Propagation; the former is used for backjumping, and the latter is used to construct a new clause to add upon finding a contradiction.