Unit Propagation
Backlinks
Conflict-Driven Clause Learning