Motivation, Definition

viele Scheduling-Probleme enthalten:

• Tätigkeit i dauert d_i Stunden
• i muß beendet sein, bevor j beginnt.

das führt zu Constraintsystem:

• Unbekannte: t_i = Beginn von i
• Constraints: t_j$\ge$t_i + d_i

STM-LIB-Logik QF_IDL, QF_RDL:

boolesche Kombination von Unbekannte$\ge$Unbekannte + Konstante