Constraint-Programmierung (Bsp: SMT)

(satisfiability modulo theory)

Programm (Constraint-System)

(set-logic QF_NIA)(set-option :produce-models true)
(declare-fun P () Int) (declare-fun Q () Int)
(declare-fun R () Int) (declare-fun S () Int)
(assert (and (< 0 P) (<= 0 Q) (< 0 R) (<= 0 S)))
(assert (> (+ (* P S) Q) (+ (* R Q) S)))
(check-sat)(get-value (P Q R S))

(ausführen mit z3 p.smt2)

Antwort (erfüllende Belegung):

sat
((P 14)  (Q 9) (R 11)  (S 7))

siehe http://z3.codeplex.com/wikipage?title=Publications