CP-Anwendung: Polynom-Interpretationen

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

  Beispiel-Rechnung: abab→baab→baba→bbaa mathend000#

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

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

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