\begin{slide}{Motivation, Definition}

viele Scheduling-Probleme enthalten:
\begin{itemize}
\item Tätigkeit $i$ dauert $d_i$ Stunden
\item $i$ muß beendet sein, bevor $j$ beginnt.
\end{itemize}
das führt zu Constraintsystem:
\begin{itemize}
\item Unbekannte: $t_i =$ Beginn von $i$
\item Constraints: $t_j \ge t_i + d_i$
\end{itemize}

STM-LIB-Logik \verb|QF_IDL, QF_RDL|:

boolesche Kombination von 
$ \text{Unbekannte} 
\ge \text{Unbekannte} + \text{Konstante}$

\end{slide}

