Wettlauf der Stundenpläne

Die Zeit der Setzkästen für Stundenpläne ist vorbei — oder nicht? Selbst moderne Computerprogramme zur Erstellung von Stundenplänen für Schulen arbeiten sehr oft mit einer Setz-Heuristik. D.h. Algorithmen versuchen, die Arbeit des Stundenplaners zu simulieren, indem Stunden nacheinander platziert werden und stets gegen die vorgegebenen Bedingungen überprüft werden. Also: „Setzkasten 2.0“. Die Zukunft der Stundenplan-Erstellung sieht meiner Ansicht nach völlig anders aus.

„Trial and Error“ vs. „Ganz oder gar nicht“.

Der oben erwähnte virtuelle Kollege am Setzkasten wird abgelöst durch einen Encoder, der Stundenplan-Vorgaben jeweils in ein umfangreiches Gleichungssysteme umwandelt, ein sogenanntes SAT-Problem (SAT = Satisfiability). Dieses Gleichungssystem muss dann von ausgeklügelten Algorithmen (einer KI, der Cloud, einem Cluster …) gelöst werden. Die Algorithmen, die diese Problem versuchen zu lösen heißen SAT-Solver. (Warum diese notwendigerweise ausgeklügelt sein müssen wir später erklärt.) Das Ergebnis ist eine Reihe von Zahlen, die eine Lösung des Gleichungssystems darstellen und vom Decoder wieder in lesbare Stundenplandaten konvertiert werden.

Ausschnitt aus einem Berechnungsergebnis eines SAT-Solvers für einen neuen Stundenplan im CNF DIMACS Format. Die Zahlen stehen für Indizes von booleschen Variablen, das Vorzeichen gibt an, ob der Variablenwert true oder false ist. Lesbar werden die Daten erst nach dem Decodieren auf dem lokalen Verwaltungsrechner.

Der Clou dabei ist der, dass diese Methode nicht inkrementell funktioniert, indem Stunden nach und nach gesetzt werden, sondern es werden alle Bedingungen gleichzeitig erfüllt. Das bedeutet: Entweder werden alle Vorgaben des Planers berücksichtigt oder es kann kein Plan erstellt werden.

Bei den üblichen Setzprogrammen ist dies nicht so; hier sind die Vorgaben oft als Richtlinien zu sehen, gegen der Algorithmus auch verstoßen kann, so dass manuelle Nacharbeiten zwangsläufig nötig sind.

Workflow

Wir nutzen an unserer Schule die über lange Jahre stetig gepflegt und fantastische Software MacStupas5 für macOS von Bernard Schriek. Diese verfügt nun über Encoder, Decoder und einige kompilierte Open Source SAT-Solver (Plingeling, CryptoMiniSat, Glucose-Syrup). Damit lassen sich Pläne in annehmbarer Zeit rechnen.

Die Vorgehensweise bei der Erstellung der Pläne ist durchaus anders als zuvor. Grob: Zunächst werden alle geforderten Voreinstellungen vorgenommen, dann wird der Plan gerechnet, und anschließend dann (manuell) geprüft.
Dies ist mag zwar sehr ähnlich zur Herangehensweise mit anderen Programmen erscheinen; ein entscheidender Unterschied liegt aber etwa in der Bedeutung des vorbereitenden Schritts: Hier darf es an keiner Stelle in den Einstellungen widersprüchliche Voreinstellungen geben, da es sonst keine Lösung des zugehörigen Gleichungssystem gäbe.

Als einfaches, offensichtliches Beispiel: Ist bei der Klasse 9a die 7. Stunde als Mittagspause geblockt, und besagt die Einstellung aber, dass der Klassenplan keine Freistunden enthalten darf, so wird kein Plan zustandekommen, da die 9er Klassen mehr als 30 Stunden pro Woche unterrichtet werden, was zwangsläufig Nachmittagsunterricht bedeutet. Aufgrund der Sperrung der 7. Stunde würde aber zwangsläufig eine Freistunde entstehen.

SAT-Encoder von MacStupas5 mit allen relevanten, aktivierten Bedingungen.

In so einem Fall würde das zugehörige Gleichungssystem vom SAT-Solver als „unsatisfiable“ erkannt und es würde kein Plan generiert. Bei einer Setz-Heuristik könnte ein Algorithmus gegen diese Bedingung verstoßen.

Der Arbeitsfluss ist also der, dass zunächst sämtliche Bedingungen für Klassen, Kurse, Lehrer und Räume vorgenommen werden und diese dann von mir Schritt für Schritt aktiviert werden, um eventuelle Widersprüche aufzudecken.

Wurden dann die möglichen Widersprüche entfernt, kann der Gesamtplan gerechnet werden. Was aus informatischer Sicht nicht simpel ist; mehr dazu im nächsten Abschnitt.

Ein weiterer Unterschied liegt bei der Begutachtung der Pläne. Da die Ergebnisse bei sorgfältiger Einarbeitung der Vorgaben oft sehr gut verwendbar sind, und die Ergebnisse zudem in relative kurzer Zeit vorliegen, stelle ich Pläne direkt massenweise her. So kommt es oft vor, dass es für ein Schuljahr 40-50 Pläne gibt, die dann von der Schulleitung verglichen und geprüft werden, z.B. hinsichtlich Verteilung der Hauptfächer in den Klassen oder auch Platzierung der Nachmittagsstunden. Da die SAT-Solver nicht-deterministisch arbeiten, variieren die Pläne entsprechend. Der Plan mit dem besten Ranking wird dann weiter bearbeitet.

NP harte Probleme…

Das Erfüllbarkeitsproblem stellt in der theoretischen Informatik nach dem Satz von Cook-Levin ein sogenanntes NP-vollständiges Problem dar. Das bedeutet grob, dass bei der (linearen) Zunahme der Eingabegröße der Rechenaufwand exponentiell (unbegrenzt) steigt.

Um die Ausmaße deutlich zu machen: Ein vollständiger Plan mit allen Vorgaben wird vom Encoder in ein boolesches Gleichungssystem (in konjunktiver Normalform) mit über 1 Millionen Variablen und teils weit über 3 Millionen Gleichungen übersetzt.

Bei einem vollen Plan steigt die Anzahl der Variablen schnell auf über 1 Millionen.

Würde man ganz naiv an die Lösung des Problems mit 1 Mio. Variablen gehen und sämtliche Belegungsmöglichkeiten dieser Variablen (jeweils wahr oder falsch) durchprobieren, so gäbe es hierfür 2^1000000 Möglichkeiten. Das entspricht einer Zahl mit mehr als 300 000 Dezimalstellen. Zum Vergleich: Die Anzahl der Atome im Universum wird auf eine Zahl mit weniger als 90 Dezimalstellen geschätzt.

…und intelligente Lösungen

Das es für derart komplexe Anforderungen dennoch Algorithmen gibt, die Lösungen für solche Probleme finden, hat die Entwickler-Gemeinde der SAT-Solver in den vergangenen Jahren gezeigt.

Jährlich treffen sich internationale Entwicklerteams von Universitäten rund um den Globus, um ihre Algorithmen gegeneinander antreten zu lassen.

Da hier MacStupas5 den Export des Gleichungssystems in Form einer .cnf-Datei bietet, ist es hier möglich, jedes Jahr den aktuellen Gewinner des jährlichen SAT-Wettbewerbs zu kompilieren und dann das SAT Problem lösen zu lassen, ggf. auch auf Großrechnern mit >=64 Prozessorkernen.

CryptoMiniSat auf 64 Kernen bei der Arbeit…

Die Rechenzeit eines vollen Plans liegt auf einer m4.16xlarge Instanz in der AWS bei etwa 2 Stunden, bei Verwendung von CryptoMiniSat mit 64 Threads. Ein herkömmlicher 4-Kern Intel iMac benötigt hier zwischen 12 und 32 Stunden.

Der aktuelle Gewinner „Kissat MAB“ des Main Tracks der SAT Competition 2021 liefert hier überraschenderweise auch gute Zeiten von teils deutlich unter 12 Stunden für einen vollen Plan auf einem M1 Prozessor, was um so erstaunlicher ist, da dieser Algorithmus nur auf einem Kern läuft.

In diesem Umfeld wird es auch in Zukunft interessante Neuerungen geben. So existieren bereits Konzepte für Algorithmen, die auf Quanten-Computern und KI Modellen für neuronale Netze basieren.

Und im nächsten Jahr heißt es dann wieder: Wer hat das Rennen im SAT Race 2022 gemacht?