Nächste Seite:
Bitblasting
Aufwärts:
Constraint-Programmierung
Vorherige Seite:
Beispiel SAT-Codierung
SMT (SAT modulo Theories)
lineare Gleichungen
Gauss-Elimination
lineare Ungleichungen
Simplex-Verfahren, Ellipsoid-Methode
Polynom(un)gleichungen
über reellen Zahlen: Satz von Tarski, zylindrische algebraische Zerlegung (QEP-CAD)
über ganzen Zahlen: 10. Hilbertsches Problem, Satz von Matiasevich/Roberts
vgl.
http://www.smtcomp.org/2009/
Johannes Waldmann 2010-01-25