- (wie bisher) Boolesche Kombinationen
werden durch DPLL(T) behandelt,
- der Theorie-Löser behandelt Konjunktionen
von Differenz-Konstraints.
- deren Lösbarkeit ist in Polynomialzeit entscheidbar,
- Hilfsmittel: Graphentheorie (kürzeste Wege),
schon lange bekannt (Bellman 1958, Ford 1960),
2009-06-22
