bei jedem Konflikt:
- (minimale) Ursache
(d. h. partielle Belegung) feststellen
- Implementierung: (partieller) Implikationsgraph
- Knoten: Literal mit decision-level
- Kanten: Unit-Progagation-Schritte
- Negation der Konfliktursache
als neue Klausel hinzufügen
conflict-driven backtracking:
- Backjump zum zweit-tiefsten decision level
der gelernten Konfliktklausel
2014-03-31
