- (später:) Boolesche Kombinationen
werden durch DPLL(T) behandelt,
- (jetzt:) 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),
2014-03-31
