Refactoring Varisat: 3. Conflict Driven Clause Learning
jix.one