Lösungsansätze

(= Projektthemen)

• simulieren als MIP, dann lösen mit glpk oder scip
• SMT/QFLRA, QFLIA, dann lösen mit (z. B.) Z3.2
• (,,bitblasting``, SMT/QFBV oder direkt nach SAT)

Literatur:

• Definition, Competition (SMT/LIB, /COMP, /EXEC) http://www.smtexec.org/exec/?jobs=311
• ,,SMT als Buch``: Daniel Kroening und Oliver Strichman: Decision Procedures--an Algorithmic Point of View, Springer 2008. http://www.decision-procedures.org/