💻 computer science

Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

Diese Arbeit führt kompakte SAT- und MaxSAT-Kodierungen für die Business-to-Business-Terminplanung ein, die Domänenfilterung und gemeinsame Variablen nutzen, um die Klauselanzahl und den Speicherverbrauch signifikant zu reduzieren und gleichzeitig die Leerlaufzeiten der Teilnehmer zu minimieren, wobei sie sowohl eine veröffentlichte MaxSAT-Formulierung als auch den kommerziellen Solver Gurobi in der Lösungs-Effizienz übertreffen.

Ursprüngliche Autoren: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Veröffentlicht 2026-08-04

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind der ultimative Partyplaner für eine riesige, hochkarätige Geschäftskonferenz. Sie haben Hunderte von Menschen, die Einzelgespräche führen müssen, aber jeder hat einen anderen Zeitplan, einige Räume sind winzig klein, während andere riesig sind, und bestimmte Besprechungen müssen stattfinden, bevor andere beginnen können. Ihr Ziel ist nicht nur, dass jeder ein Treffen bekommt; Ihr Ziel ist es auch sicherzustellen, dass niemand zwischen seinen Terminen zu lange gelangweilt herumsitzt. Dies ist das chaotische Puzzle der „Business-to-Business (B2B) Meeting-Planung“.

Um dieses Problem zu lösen, verwenden Informatiker eine spezielle Art von Logikspiel namens SAT (Erfüllbarkeit). Denken Sie an SAT als einen superintelligenten Detektiv, der prüft, ob eine Menge von Regeln jemals gleichzeitig wahr sein kann. Wenn Sie dem Detektiv sagen: „Meeting A muss vor Meeting B stattfinden, aber Meeting B muss vor Meeting A stattfinden“, sagt der Detektiv sofort: „Unmöglich!“ Aber wenn die Regeln knifflig, aber möglich sind, findet der Detektiv einen gültigen Zeitplan. Eine andere Version, MaxSAT, ist wie ein Detektiv, der nicht nur einen gültigen Zeitplan findet, sondern auch versucht, ihn perfekt zu machen, indem er minimiert, wie viel Zeit die Leute mit Warten verbringen. Diese Arbeit vertieft, wie wir diese logischen Detektive schneller und klüger machen können, wenn wir solche komplexen geschäftlichen Ereignisse organisieren.

Das Problem: Ein verworrenes Netz aus Meetings

In der Welt der Geschäftstermine wird es schnell unordentlich. Sie haben eine Liste von Meetings, eine Liste von Zeitslots und eine Liste von Räumen. Die Regeln sind streng:

Keine Überschneidung: Eine Person kann nicht an zwei Orten gleichzeitig sein.
Raumbeschränkungen: Ein Raum kann nicht mehr Meetings beherbergen, als seine Kapazität zulässt.
Präzedenz (Vorgängigkeit): Einige Meetings müssen vor anderen stattfinden (wie eine morgendliche Besprechung vor einem Nachmittags-Workshop).
Das „Leerlauf“-Problem: Das eigentliche Kopfzerbrechen ist die „Leerlaufzeit“ (Idle Time). Wenn ein Teilnehmer ein Meeting um 9:00 Uhr hat und sein nächstes erst um 11:00 Uhr stattfind, hat er zwei Stunden „Leerlaufzeit“. Das Ziel dieser Forschung ist es, dies so auszubalancieren, dass niemand stundenlang wartet, während andere nur wenige Minuten warten. Es geht um Fairness und Effizienz.

Der alte Weg vs. der neue Weg

Die Forscher untersuchten eine bestehende Methode (genannt ORG-MAXSAT), die bereits ziemlich gut war. Sie stellten jedoch fest, dass es so war, als würde man versuchen, eine Party zu organisieren, indem man jede einzelne mögliche Kombination von Gästen und Zeiten aufschreibt, selbst die, die offensichtlich unmöglich sind. Es war sperrig, langsam und verbrauchte viel Computerarbeitsspeicher.

Das Team der VNU University of Engineering and Technology in Vietnam beschloss, eine „kompakte“ Version zu entwickeln. Sie führten drei Haupttricks ein, um das Problem zu verkleinern:

Der „Vorab-Check“-Filter (Domänenfilterung): Bevor sie den Computer-Detektiv überhaupt mit dem Lösen des Puzzles beauftragen, fügten sie einen smarten Filter hinzu. Dieser Filter betrachtet die Regeln und streicht sofort unmögliche Optionen durch. Wenn zum Beispiel ein Meeting nach einem anderen stattfinden muss, das um 14:00 Uhr endet, entfernt der Filter sofort alle Zeitslots vor 14:00 Uhr aus der Liste der Möglichkeiten. Das ist wie das Aufräumen eines Schreibtisches, bevor man versucht, einen bestimmten Stift zu finden. Sie bewiesen, dass dieser Filter niemals eine gültige Lösung wegwirft; er entfernt nur den Müll.
Die „Gemeinsame Treppe“ (Sparse Shared-Suffix Encoding): Beim Umgang mit den „muss vor ... stattfinden“-Regeln schrieb die alte Methode eine separate Notiz für jedes einzelne Paar von Meetings auf. Wenn man 100 Meetings hatte, waren das tausende von Notizen. Die neue Methode bemerkte, dass viele dieser Notizen das Gleiche sagten. Anstatt separat zu schreiben „Meeting A vor B“, „Meeting A vor C“ und „Meeting A vor D“, erstellten sie eine gemeinsame „Treppe“ der Logik. Sie nutzen Variablen für ähnliche Situationen wieder, wie etwa die Verwendung eines Generalschlüssels für mehrere Türen anstelle, für jedes einzelne Schloss einen neuen Schlüssel zu fertigen.
Der „Fairness“-Score (Leerlaufzeit-Ausgleich): Anstatt nur die Anzahl der Pausen einer Person zu zählen, entwickelten sie eine neue Art, die „Leerlaufzeit“ zu messen. Sie betrachteten die Zeit zwischen dem ersten und dem letzten Meeting einer Person. Wenn jemand Meetings um 9:00 und 11:00 Uhr hat, beträgt die „Spanne“ zwei Stunden. Wenn jemand nur ein einziges Meeting hatte, hat er null Leerlaufzeit. Das Ziel ist es, den Unterschied zwischen der Leerlaufzeit der am stärksten beschäftigten Person und der am wenigsten beschäftigten Person so gering wie möglich zu halten.

Was sie herausfanden

Die Forscher testeten ihre neue „kompakte“ Methode gegen die alte Methode und gegen einige sehr leistungsstarke kommerzielle Software (wie Gurobi und CPLEX) in 126 offiziellen Testfällen und 100 zusätzlichen „Stresstest“-Fällen mit noch mehr Meetings.

Hier sind die Ergebnisse, die durchaus beeindruckend sind:

Kleinere Größe: Die neue Methode reduzierte die Anzahl der logischen „Klauseln“ (die Regeln, die der Computer prüfen muss) im Durchschnitt um 40,3 %.
Weniger Speicher: Sie verbrauchte 55,9 % weniger Spitzenarbeitsspeicher. Stellen Sie sich vor, man benötigt nur halb so viel RAM, um dasselbe Puzzle zu lösen.
Schnellere Geschwindigkeit: Die Gesamtlösungszeit für die Probleme sank um 14,0 %.
Die Kraft der Filterung: Allein durch den Einsatz des „Vorab-Check“-Filters wurden die Anzahl der Variablen um 24,1 % und die Regeln um 16,2 % reduziert.
Die Kraft des Teilens: Der „Gemeinsame Treppe“-Trick reduzierte die Anzahl der Regeln um weitere 0,5 % bis 5,5 %, abhängig davon, wie voll der Zeitplan war.

Das Urteil

Der spannendste Teil ist, dass ihre neuen kompakten SAT- und MaxSAT-Methoden in der Lage waren, jeden einzelnen der 126 offiziellen Testfälle zu lösen. Noch besser: Sie taten dies schneller als den führenden kommerziellen Solver Gurobi in Bezug auf die Medianzeit. Während andere kommerzielle Tools (wie CPLEX und CP Optimizer) Schwierigkeiten hatten, alle Fälle innerhalb des Zeitlimits zu lösen, bewältigte der neue SAT-basierte Ansatz sie alle.

Die Arbeit behauptet nicht, die Scheduling-Probleme des Universums für immer gelöst zu haben, aber sie hat definitiv gezeigt, dass wir durch das Aufräumen der Regeln und das intelligentere Teilen der Arbeit Computer viel besser darin machen können, unser geschäftiges Leben zu organisieren. Sie verwandelt einen massiven, verworrenen Knoten aus Meetings in einen ordentlichen, ausgewogenen Zeitplan, bei dem jeder seinen fairen Anteil an Zeit bekommt und niemand zu lange im Flur warten muss.

Technisches Resümee: Kompakte SAT- und MaxSAT-Kodierungen für das B2B-Meeting-Scheduling mit Ausgleich der Leerzeit

Problemdefinition

Die Arbeit befasst sich mit dem Business-to-Business (B2B) Meeting-Scheduling, einem kombinatorischen Optimierungsproblem, bei dem angeforderte paarweise Meetings spezifischen Zeitslots und Standorten zugewiesen werden müssen. Das Scheduling muss mehrere Constraints erfüllen:

Nicht-Überlappung der Teilnehmer: Ein Teilnehmer kann nicht zwei Meetings gleichzeitig wahrnehmen.
Kapazität der Standorte: Die Anzahl der Meetings in einem beliebigen Zeitslot darf die Anzahl der verfügbaren Standorte ( $K$ ) nicht überschreiten.
Verfügbarkeit & Einschränkungen: Meetings müssen innerhalb angeforderter Sitzungen, fester Slots oder unter Ausschluss verbotener Slots stattfinden.
Präzedenz: Gerichtete Kanten $(i, j)$ erzwingen, dass Meeting $i$ vor Meeting $j$ stattfinden muss.

Das in dieser Arbeit vorgeschlagene Ziel unterscheidet sich von früheren Formulierungen (die oft „Break-Gruppen“ minimieren oder die Disparität in der Anzahl der Pausen begrenzen). Stattdessen minimiert diese Studie die Spanne der internen Leerzeit-Summen ( $\Delta I$ ) unter den Teilnehmern, die mindestens zwei Meetings haben. Interne Leerzeiten sind definiert als ungenutzte Zeit zwischen dem ersten und dem letzten zugewiesenen Meeting eines Teilnehmers. Diese Metrik unterscheidet zwischen kurzen Unterbrechungen und längeren Wartezeiten und zielt auf eine ausgewogene Lastverteilung ab, ähnlich dem Balanced Academic Curriculum Problem (BACP). Ein aggregiertes Maß für die Leerzeit ( $I_\Sigma$ ) wird ebenfalls als ergänzende Metrik angegeben.

Methodik

Die Autoren schlagen eine kompakte SAT (Boolean Satisfiability) und MaxSAT Kodierung vor, die drei primäre Modellierungsverbesserungen gegenüber bestehenden veröffentlichten Formulierungen integriert:

Lösungserhaltende Domänenfilterung (Preprocessing):
Vor der Erzeugung der Konjunktiven Normalform (CNF) wenden die Autoren einen Vorverarbeitungsalgorithmus (Algorithmus 1) an, der nicht unterstützte Zuweisungen entfernt. Dieser integriert:
- Endpunkt-gebundene Filter: Propagation von Präzedenz-Constraints entlang von Pfaden (unter Verwendung direkter Kanten oder des transitiven Abschlusses).
- Pro-Teilnehmer-Matching: Entfernung von Zuweisungen, die nicht Teil eines konfliktfreien Schedules für einen spezifischen Teilnehmer sein können.
- Gesättigte-Slot-Propagation: Eliminierung von Slots, in denen die Kapazität bereits durch erzwungene Zuweisungen voll ausgelastet ist.
- Behauptung: Dieser Prozess bewahrt alle zulässigen Schedules bei gleichzeitiger Reduzierung der Domänengröße, wodurch die Anzahl der Variablen und Klauseln sinkt.
Sparse Shared-Suffix Precedence Encoding (SPARSESUFFIX):
Anstatt Präzedenzrelationen mittels paarweiser Klauseln zu kodieren (was quadratisch in der Domänengröße sein kann), führen die Autoren eine spärliche Kodierung ein.
- Sie materialisiert nur die distinkten „Schnittpunkte“ im Präzedenz-Bereich, an denen die Constraint aktiv wird.
- Sie nutzt Hilfsvariablen für identische Schnitte über verschiedene Relationen hinweg wieder.
- Dieser Ansatz ist nachweislich äquivalent zu paarweisen Klauseln, reduziert jedoch die Klauselanzahl erheblich, insbesondere in Kombination mit der Domänenreduktion.
Bereichsbasierte Leerzeit-Zielgröße:
Das Paper führt eine exakte Kodierung zur Minimierung der Spanne der internen Leerzeiten ( $\Delta I$ ) ein.
- Es leitet die ersten und letzten besetzten Slots für jeden Teilnehmer ab.
- Es verwendet eine lineare Anzahl an Hilfsvariablen, um die Differenz zwischen der maximalen und minimalen Leerzeit-Anzahl über alle relevanten Teilnehmer hinweg zu berechnen.

Die Studie evaluiert diese Komponenten gegen eine Baseline-ORG-MAXSAT Formulierung (eine Anpassung eines veröffentlichten Modells) und kommerzielle Solver (Gurobi, CPLEX, CP Optimizer). Die Evaluierung umfasst 126 offizielle Benchmark-Instanzen und 100 abgeleitete „Stress“-Instanzen mit variierenden Präzedenz-Dichten.

Kernbeiträge

Das Paper identifiziert drei spezifische Beiträge:

Preprocessing-Verfahren: Ein Filter-Integrationsverfahren, das nicht unterstützte Zuweisungen vor der CNF-Generierung entfernt. Proposition 1 beweist, dass dies die Zulässigkeit bewahrt, und empirische Ergebnisse zeigen, dass es die Zuweisungsvariablen um 24,1 % und die Klauseln um 16,2 % reduziert.
Sparse Shared-Suffix Repräsentation: Eine exakte Kodierung (SPARSESUFFIX), die nur die erforderlichen Schnittpunkte der Präzedenz-Domäne materialisiert. Proposition 3 beweist die Äquivalenz zu paarweisen Klauseln. Die Studie zeigt, dass die Domänenreduktion zwar die Variablenanzahl senkt, das Suffix-Sharing jedoch unabhängig die Klauselanzahl reduziert.
B2B-spezifische Zielgröße: Eine bereichsbasierte Leerzeit-Zielgröße, die die Disparität der internen Wartezeiten misst und mit einer linearen Anzahl an Hilfsvariablen kodiert ist.

Experimentelle Ergebnisse

Die Experimente wurden auf einer 4-Kern-Maschine mit einem Zeitlimit von 7.200 Sekunden durchgeführt. Zentrale Erkenntnisse sind:

Formelgröße und Speicher: Im Vergleich zur angepassten ORG-MAXSAT-Baseline reduzierte die vorgeschlagene kompakte Kodierung die mediane Klauselanzahl um 40,3 % und den medianen Spitzen-Speicherverbrauch um 55,9 %.
Auswirkung der Domänenreduktion: Die Domänenfilterung allein reduzierte die Zuweisungsvariablen um 24,1 % und die Klauseln um 16,2 %, was den größten Anteil an der Reduktion der Formelgröße ausmachte.
Präzedenz-Kodierung: Die SPARSESUFFIX-Kodierung reduzierte die mediane Klauselanzahl um 0,5 %–1,0 % bei offiziellen Präzedenz-Instanzen und um bis zu 5,5 % bei den am dichtesten besetzten abgeleiteten Instanzen (in Kombination mit dem transitiven Abschluss).
Solver-Performance:
- Alle drei vorgeschlagenen SAT/MaxSAT-Methoden (inkrementelles SAT, nicht-inkrementelles SAT und UWrMaxSAT) lösten alle 126 offiziellen Instanzen.
- Im Vergleich zu Gurobi (dem einzigen kommerziellen Solver, der alle Instanzen löste), erreichten die vorgeschlagenen SAT/MaxSAT-Methoden geringere mediane Gesamtlaufzeiten.
- Inkrementelles SAT erreichte die niedrigste mediane Zeit (0,227 s) unter den vollständigen Methoden.
- CP Optimizer hatte die niedrigste mediane Zeit (0,110 s), konnte aber 11 Instanzen innerhalb des Zeitlimits nicht lösen.

Bedeutung und Behauptungen

Das Paper behauptet, dass die vorgeschlagene kompakte Kodierung eine signifikante Effizienzsteigerung gegenüber bestehenden Booleschen Formulierungen für das B2B-Meeting-Scheduling bietet. Durch die Trennung der Domänenfilterung von der Präzedenzrepräsentation demonstrieren die Autoren, dass die Domänenreduktion der primäre Treiber für die Reduzierung der Formelgröße ist, während die Sparse Shared-Suffix-Kodierung eine zusätzliche, unabhängige Reduktion der Klauseln ermöglicht.

Die Studie stellt fest, dass die neue Leerzeit-Spannen-Zielgröße ein nuancierteres Maß für die Qualität eines Schedules liefert als bisherige „Break-Group“-Metriken, da sie zwischen kurzen Unterbrechungen und langen Wartezeiten unterscheidet. Darüber hinaus deuten die Ergebnisse darauf hin, dass moderne SAT- und MaxSAT-Solver, wenn sie mit diesen kompakten Kodierungen ausgestattet sind, führende kommerzielle MIP- und CP-Solver in Bezug auf die mediane Lösungszeit für diese spezifische Problemklasse übertreffen können, indem sie alle Benchmark-Instanzen lösen, bei denen einige kommerzielle Solver ein Zeitlimit erreichten.

Die Autoren bleiben bescheiden hinsichtlich zukünftiger Arbeiten und merken an, dass sich die aktuelle Studie auf die Single-Run-Zeitmessung konzentriert und dass zukünftige Forschung wiederholte Zeitmessungen sowie lexikographische Zielgrößen (Minimierung von $\Delta I$ vor $I_\Sigma$ ) untersuchen könnte.