\begin{slide}{Constraint-Programmierung---Beispiel}
\begin{small}
\begin{verbatim}
(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))
\end{verbatim}
\end{small}
\begin{itemize}\itemsep 1pt
\item 
\emph{Constraint-System}
 $=$ eine prädikatenlogische Formel $F$
\item
\emph{Lösung} $=$ Modell von $F$ ($=$ Strukur $M$,
in der $F$ wahr ist)
\item
CP ist eine Form der \emph{deklarativen} Programmierung.
\item
\emph{Vorteil}: Benutzung von allgemeinen Suchverfahren
(bereichs-, aber nicht anwendungsspezifisch).
\end{itemize}

\end{slide}
