CDCL

Also known as Conflict-driven clause learning. This is the canonical page; those names redirect here.

Pairings in the atlas

VSIDS branchingcanonModern SAT solving backtracking-cp
First-UIP clause learningcanonModern SAT solving backtracking-cp
Two-watched-literal propagationstandardSAT solver engineering backtracking-cp
Luby restart schedulestandardSAT solving backtracking-cp
Phase savingstandardSAT solving backtracking-cp
LBD clause deletionspecialistSAT solving backtracking-cp

Rivals: other methods for the same problems

Where it sits

backtracking-cp · Search, Constraints & Games