Motivation, Definition

viele Scheduling-Probleme enthalten:

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

das führt zu Constraintsystem:

• Unbekannte: t_i = mathend000# Beginn von i mathend000#
• Constraints: t_j≥t_i + d_i mathend000#

STM-LIB-Logik QF_IDL, QF_RDL:

boolesche Kombination von Unbekannte≥Unbekannte + Konstante mathend000#