Solver verstehen & UNSAT lösen
Wie Prilog rechnet, was die Score-Werte bedeuten, und was Du tust wenn der Solver „Lösung nicht möglich" meldet.
Was macht der Solver?
Wenn Du Auto-Plan klickst, geht Prilog so vor:
- Backend sammelt alle Stammdaten (Klassen, Fächer, Räume, Lehrer, Zeitraster, Stundentafel, Regelwerk, Verfügbarkeiten, Couplings …) und baut daraus einen Snapshot.
- Der Snapshot wird per HTTP an den Solver-Service geschickt (eigener Python-Service mit Google OR-Tools CP-SAT).
- Der Solver baut ein mathematisches Modell mit Variablen (welche Stunde liegt wann?) und Constraints (welche Kombinationen sind erlaubt?).
- CP-SAT sucht eine Lösung mit minimalem Soft-Score, bis das Zeitbudget abläuft oder die optimale Lösung gefunden ist.
- Das Ergebnis kommt als Liste von Einträgen (Klasse + Fach + Lehrer + Raum + Slot) zurück.
CP-SAT (Constraint Programming - Boolean Satisfiability) ist das gleiche Mathe wie SAT-Solver für Software-Verifikation: ein Such-Algorithmus, der sehr viele Kombinationen schnell durchprobiert.
Hard- vs. Soft-Constraints
Hard = Verletzung verboten. Der Solver würde lieber gar keine Lösung finden als eine Hard-Verletzung produzieren.
Soft = Verletzung wird mit Penalty-Punkten („Score") bestraft. Solver versucht, den Score zu minimieren.
Aktive Hard-Constraints (Stand 2026-05-28)
| # | Constraint | Was es verbietet |
|---|---|---|
| H1 | Klasse-Slot-Konflikt | Eine Klasse hat nicht zwei Stunden zur selben Zeit (außer Halbgruppen) |
| H2 | Lehrer-Slot-Konflikt | Ein Lehrer kann nicht zwei Stunden gleichzeitig geben |
| H3 | Raum-Slot-Konflikt | Ein Raum ist nicht doppelt belegt |
| H4 | Qualifikation | Solver setzt nur qualifizierte Lehrer (TeacherQualification) |
| H5 | Raum-Tags | Sport braucht sporthalle-Tag, etc. (Subject.requiredResourceTags) |
| H6 | PeriodSlots gefiltert | Pausen-Slots werden nicht belegt |
| H7 | Manuelle Pins | Was fixiert ist, bleibt fixiert (TimetablePinConstraint) |
| H8 | Auto-Pins aus Assignment | importance=100 setzt Lehrer hart |
| H9 | Stammraum-Default | Klassen-Stammraum-Auto-Pin |
| H10 | Lock-Level Cells | Board-Cells mit pinLevel != soft → Position/Lehrer/Raum fix |
| H11 | Lehrer-Deputat | sum(Stunden) ≤ contractedHoursWeek − reductionHoursWeek |
| H12 | Lehrer-Verfügbarkeit | Lehrer wird NIE in gesperrte Slots gesetzt |
| H13 | Klassen-Regelwerk | 5 Regeltypen (subject_in_window etc.) als hard |
| H14 | A/B-Wochen | A und B konfligieren nicht im gleichen Slot, both blockiert beide |
| H15 | Couplings | Cells mit gleichem couplingKey landen im gleichen Slot |
| H16 | Stundentafel-Vollständigkeit | jede SGH-Stunde MUSS platziert werden |
Aktive Soft-Constraints (Score-Buckets)
| # | Bucket | Penalty pro Verstoß | Was gut ist |
|---|---|---|---|
| S1 | free_periods | 1 | Wenig Hohlstunden für Klassen |
| S2 | pref_grade_mismatch | 1 | Lehrer in Wunsch-Stufen (TeacherPreference) |
| S3 | missing_preferred_tags | 1 | Fach in präferiertem Raum-Tag |
| S4 | double_slot_misses | 2 | preferDoubleSlot erfüllt |
| S5 | teacher_day_overload | (geplant) | Max. Stunden pro Tag pro Lehrer |
| S6 | room_changes | 1 | Wenig Räume pro Klasse-Tag (Raum-Kontinuität) |
| S7 | preferred_room_mismatch | 1 | Lehrer im Lieblings-Raum |
score.total = Summe aller. Niedriger = besser.
Status-Werte verstehen
Der Solver liefert einen der folgenden Status:
| Status | Bedeutung | Was tun? |
|---|---|---|
optimal | Beste Lösung gefunden, kein Constraint verletzt | Vorschlag übernehmen 🎉 |
feasible | Funktionierende Lösung gefunden, vielleicht nicht optimal | Vorschlag prüfen, ggf. nochmal mit längerem Timeout |
infeasible | Mathematisch keine Lösung — irgendwo widersprechen sich Constraints | Diagnose lesen, siehe unten |
timeout | Zeitbudget abgelaufen, keine Lösung gefunden | Timeout erhöhen oder Hard-Constraints lockern |
error | Modell-Aufbau gescheitert (z.B. kein qualifizierter Lehrer) | Stammdaten-Fehler — Bereitschafts-Check |
UNSAT-Diagnose lesen
Wenn Status infeasible ist, schaut Prilog automatisch im Job-Result-Log nach Diagnose-Hinweisen. Die Diagnose-Funktion diagnoseInfeasible prüft die zwei häufigsten Ursachen:
Diagnose-Typ 1: Deputat-Engpass
Auslöser: Die Summe aller Lehrer-Caps für ein Fach reicht nicht für den Stundentafel-Bedarf.
Beispiel-Meldung:
Fach „Mathematik": 24h Bedarf, qualifizierte Lehrer mit Cap-Summe 18h:
Frau Schmidt (12h), Herr Müller (6h). Deputat erhöhen oder Quali ergänzen.Was tun:
- Deputat-Wert erhöhen bei Frau Schmidt oder Herrn Müller (Sub-Panel „Deputat")
- Weitere Mathe-Lehrer qualifizieren (Sub-Panel „Qualifikationen")
- Stundentafel reduzieren in einer Klasse (1h weniger Mathe)
Diagnose-Typ 2: Verfügbarkeits-Engpass
Auslöser: Lehrer-Cap > verbleibende Slots nach Sperren.
Beispiel-Meldung:
Lehrer „Frau Müller": Cap 24h/Woche, aber nur 20 Slots nach Sperren
verfügbar (15 blockiert). Sperren reduzieren oder Cap nachjustieren.Was tun:
- Sperren reduzieren in der Verfügbarkeitsmatrix
- Cap nachjustieren falls realistisch (Teilzeit 50% bei 28h Vollzeit-Vertrag = 14h ist OK)
Wenn keine Diagnose im Log steht
Dann ist die Ursache woanders. Häufige Fälle:
Klassen-Regelwerk widersprüchlich
Du hast „Hauptunterricht 1./2." als Tenant-Default UND „Mathe nicht nach Hauptunterricht" als Reihenfolge-Verbot. → Mathe darf dann nie in Slot 3 liegen — und das wird schnell unerfüllbar.
Check: Klassen-Regelwerk → alle aktiven Regeln durchgehen. Wenn keine widersprechen sollten, eine deaktivieren und nochmal solven.
Cell-Locks widersprüchlich
Du hast 5a Mo-1 + 5a Mo-2 + 5a Mo-3 als 🔒 alles fix mit verschiedenen Lehrern, die alle nur Mo-1 verfügbar sind.
Check: Klassen-Vorlage → fixierte Cells durchgehen. Mit 📌 Tag+Slot statt 🔒 Alles fix arbeiten lassen.
Stundentafel größer als Raster
Klasse 5a hat 38h Wochenstunden Bedarf, aber das Zeitraster bietet nur 35 Slots Mo–Fr.
Check: Bereitschafts-Diagnose → „Klassen-Slots vs. Stundentafel-Soll".
Coupling unerfüllbar
5a Mi-4 mit
rel-5er, 5b Mi-4 mitrel-5er— aber 5b Mi-4 ist schon mit🔒 Alles fixfür ein anderes Fach belegt.
Check: Klassen-Vorlage → Coupling-Badge (🔗) auf allen Klassen prüfen, ob die Slots wirklich frei sind.
Score-Werte richtig interpretieren
„Score 0" ist nicht immer erreichbar
Manche Score-Buckets sind strukturell nicht-0:
room_changesist mindestens (Klassen × Tage), weil jede Klasse pro Tag mindestens 1 Raum benutzt. Bei 20 Klassen × 5 Tagen = 100 Min-Wert.preferred_room_mismatchkann hoch sein wenn viele Lehrer denselben Wunsch-Raum haben — nur eine Person bekommt ihn.
Beim Vergleichen mehrerer Auto-Pläne ist die Differenz wichtig, nicht der absolute Wert.
Welche Bucket-Werte sind „kritisch"?
| Bucket | „Kritisch" ab | Was es bedeutet |
|---|---|---|
free_periods | > 0.5 × Klassen-Anzahl | Mehr als eine Hohlstunde pro Klasse pro Woche im Schnitt |
pref_grade_mismatch | > 0.3 × Stunden-Anzahl | 30%+ der Stunden ignoriert Lehrer-Stufen-Wunsch |
missing_preferred_tags | > 5 | Pro 5 Stunden eine Soft-Tag-Missachtung |
double_slot_misses | > 2 × preferDoubleSlot-Fächer | Doppelstunde-Wunsch nicht erfüllt |
room_changes | > 2 × (Klassen × Tage) | Klassen wechseln >2 Räume pro Tag im Schnitt |
preferred_room_mismatch | > 0.2 × Lehrer-mit-Pref-Raum-Stunden | 20%+ Wunsch-Raum nicht erfüllt |
Diese Schwellen sind grobe Faustregeln. Solver-Output optimal ist immer akzeptabel — die Schwellen sind nur Indikatoren für „könnte besser sein".
Performance-Tipps
Zeitbudget wählen
| Schulgröße | Empfohlenes Timeout |
|---|---|
| < 100 Schüler, ≤ 10 Klassen | 30s |
| 100–500 Schüler, 10–25 Klassen | 60–120s |
| 500–1000 Schüler, 25–50 Klassen | 180–300s |
| > 1000 Schüler, > 50 Klassen | 300–600s |
Faustregel: ab score.total sich nicht mehr ändert über 2 Minuten ist das Optimum vermutlich erreicht.
Was reduziert Solve-Zeit?
- Mehr Pins: jeder fixierte Cell ist ein nicht-Such-Punkt.
- Stammraum-Default: pinnt automatisch Klassen-Räume.
- Strikte Qualifikationen: weniger Lehrer-Optionen pro Fach.
- Größeres Zeitraster: mehr freie Slots pro Klasse.
Was erhöht Solve-Zeit?
- Viele Halbgruppen mit Rotation: produziert doppelte/dreifache Plan-Slots.
- Viele Couplings: jede Coupling-Gruppe erzeugt Constraint-Block.
- Raum-Wechsel-Minimierung: viele BoolVars pro (Klasse × Tag × Raum).
- Lehrer-Verfügbarkeits-Sperren: jeder Sperr-Slot ist ein Constraint.
Output verstehen — was zurückkommt
SolverResponse enthält:
status— siehe Tabelle obenentries[]— die platzierten Stunden, jeder mit:classSpaceId,subjectId,teacherId,roomId,slotIdweekday,orderIndex(Mo=0…Fr=4, Slot-Position im Tag)weekParity—both/A/B
unplaced[]— Stunden, die NICHT platziert werden konntenclassSpaceId,subjectId,requiredHours,placedHours,reason
score— Soft-Score-Buckets (siehe oben)log[]— Diagnose-Text, vor allem beiinfeasibleinteressantsolverWallSeconds— wie lange CP-SAT gerechnet hat
Im Backend wird entries[] über den Accept-Workflow (Knopf „Vorschlag übernehmen") in TimetableEntry-Rows umgesetzt — mit planningStatus=draft.
Anhang: Architektur
- Backend (
prilog-backend-api): bauteilt das Payload inbuildSolveInput(solve-job.service.ts). - Solver-Worker (separater pm2-Service): pollt
TimetableSolveJob-Tabelle alle 2s, übernimmtqueued-Jobs, ruftrunSolve(). - Solver-Service (
prilog-stundenplan-solver, Python): läuft als Docker-Containerprilog/stundenplan-solver:X.Y.Z-mtauf Whisper-Box. Health-Check via/health. - CP-SAT: Google OR-Tools, Pure-Python-Binding.
- Job-Lifecycle:
queued→running→done/failed/cancelled.
Versions-Anker per 2026-05-28: Solver 0.7.1-mt, Backend SHA af3a36d, Frontend Bundle index-DAcp3Df7.js.
Verwandt: