CP-Anwendung: Polynom-Interpretationen

• Berechnungsmodell: Wortersetzung ($\approx$ Turingmaschine)
• Programm: ab→ba ($\approx$ Bubble-Sort)

  Beispiel-Rechnung: abab→baab→baba→bbaa

• Bewertung W durch lineare Funktionen f_a(x) = Px + Q, f_b(x) = Rx + S mit P, Q, R, S∈$\mathbb {N}$

  W(abab) = f_a(f_b(f_a(f_b(0)))),…

• monoton: x > y⇒f_a(x) > f_a(y)∧f_b(x) > f_b(y)
• kompatibel mit Programm: f_a(f_b(x) > f_b(f_a(x))
• resultierendes Constraint-System für P, Q, R, S,
• Lösung mittels Z3