Clause learning
= Clause learning
Deriving additional <Boolean clauses> implied by the original <Boolean formula>, usually after analyzing a conflict in search. A learned <Boolean clause> excludes a failed combination of choices on subsequent branches without removing any <satisfying assignment>.