Constraint-Programmierung--Beispiel

(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))

• Constraint-System = eine prädikatenlogische Formel F
• Lösung = Modell von F (= Strukur M, in der F wahr ist)
• CP ist eine Form der deklarativen Programmierung.
• Vorteil: Benutzung von allgemeinen Suchverfahren (bereichs-, aber nicht anwendungsspezifisch).