KALKÜL sucht den besten Plan, der alle Regeln hält.

Ein Optimierungsproblem hat drei Teile. Die Variablen sind die Größen, die der Plan festlegt: reelle Zahlen wie eine Menge, ganze Zahlen wie eine Anzahl, binäre Entscheidungen wie ein Ja oder Nein je Möglichkeit. Die Zielfunktion misst, was besser sein soll, und wird minimiert oder maximiert. Die Nebenbedingungen sind die Regeln, die jeder zulässige Plan einhält.

Die Nebenbedingungen werden nicht für die Optimierung neu geschrieben. Sie stammen aus denselben Regeln mit derselben Fassung und Version, die KALKÜL bei der Prüfung benutzt. Es gäbe sonst zwei Fassungen derselben Vorschrift, und die eine könnte abweichen. Harte Regeln sind Nebenbedingungen und werden nie verletzt. Weiche Regeln, also Vorlieben, gehen als Strafterm mit ausdrücklichem Gewicht in das Ziel ein.

Sind Ziel und Nebenbedingungen linear, ist das ein lineares Programm, das sich mit dem Simplex-Verfahren oder mit Innere-Punkte-Verfahren lösen lässt. Kommen ganzzahlige oder binäre Variablen hinzu, wird daraus ein gemischt-ganzzahliges Programm (MILP), für das Branch-and-Bound und Branch-and-Cut die gängigen Verfahren sind. Aufgaben mit logischen Bedingungen, etwa Reihenfolgen und Zuordnungen, löst alternativ die Constraint-Programmierung, zum Beispiel mit CP-SAT aus OR-Tools. Als Löser kommen offene wie HiGHS und SCIP in Frage; welcher läuft, steht im Nachweis.

Ein Löser liefert nicht nur eine Lösung, sondern eine Schranke: den besten Zielwert, der überhaupt noch möglich ist. Der Abstand zwischen der besten gefundenen Lösung und dieser Schranke heißt Lücke. Ist sie null, ist der Plan nachweislich optimal. Ist sie größer, ist er ein zulässiger Plan mit ehrlicher Güte, und KALKÜL nennt die Lücke und nicht nur den Plan.

Unsichere Parameter lassen sich robust behandeln: Statt eines Werts gilt ein Intervall, und der Plan muss für jeden Wert darin zulässig sein. Das verbindet die Optimierung mit der Rechnung mit Intervallen.

Ein numerischer Löser rechnet im Gleitkomma und mit Toleranzen: Eine Nebenbedingung gilt dort als erfüllt, wenn sie um nicht mehr als eine kleine Zulässigkeitstoleranz verletzt ist. Für ein Ziel ist das unerheblich, für eine Regel, die eine Grenze meint, nicht. Die Sicherheit darf nicht an einer Toleranz hängen.

KALKÜL behandelt den Plan des Optimierers darum wie jeden Vorschlag. Er wird auf die Teilung gebracht, die die Handlung kennt, und mit dem exakten Verfahren gegen dieselben Regeln geprüft, mit dem SMT-Löser oder mit Intervallen. Erst das Ergebnis dieser Prüfung ist der Nachweis. Verletzt der Plan eine Regel, geht er mit dem Gegenbeispiel an die Optimierung zurück, die eine Nebenbedingung verschärft. Der Optimierer darf irren, die Prüfung nicht.

Optimierung braucht Zeit, und die Zeit ist begrenzt. Der Löser läuft mit einem Rechenbudget und liefert, wann immer es endet, den besten bisher gefundenen zulässigen Plan mit der aktuellen Schranke. Abgebrochen wird bei Ablauf der Zeit oder wenn die Lücke eine vorgegebene Grenze unterschreitet. Beides steht im Ergebnis. Einen Plan ohne Angabe der Lücke gibt KALKÜL nicht aus.

Gibt es keinen zulässigen Plan, ist das ein eigenes Ergebnis mit eigener Aussage: Die Regeln widersprechen einander. KALKÜL nennt dann die kleinste Menge von Regeln, die zusammen keinen Plan zulassen. Löser kennen sie unter den Namen Unsatisfiable Core und Irreducible Infeasible Subsystem. Für die Pflege der Regeln ist das wertvoll, denn es zeigt, welche Vorschriften sich im Betrieb gegenseitig ausschließen.

Die Läufe sind wiederholbar. Fassung der Regeln, Version des Lösers, Einstellungen und Startwert stehen im Nachweis, und dieselben Eingaben führen bei gleicher Einstellung zum selben Plan.

Wo mehrere Ziele zählen, wird der Zielkonflikt nicht im Löser versteckt. KALKÜL kennt drei Wege: die gewichtete Summe mit sichtbaren Gewichten, die lexikografische Ordnung, die erst das erste Ziel optimiert und danach das zweite unter der Bedingung, dass das erste nicht schlechter wird, und die Pareto-Menge, also alle Pläne, die in keinem Ziel zu verbessern sind, ohne ein anderes zu verschlechtern.

Gewichte und Ordnung sind Daten mit Version und einem Verantwortlichen. Der Plan nennt, mit welchen Gewichten er entstand. Wer eine Gewichtung ändert, ändert eine Entscheidung, und das steht im Verlauf. Eine harte Regel lässt sich nie durch ein Gewicht aufwiegen; ein Plan, der sie brechen müsste, braucht eine Ausnahme mit Freigabe.