💻 computer science

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

Dit artikel introduceert compacte SAT- en MaxSAT-encoderingen voor zakelijke vergaderplanning die gebruikmaken van domeinfiltering en gedeelde variabelen om het aantal clausules en het geheugengebruik aanzienlijk te verminderen, terwijl de inactiviteitstijden van deelnemers worden geminimaliseerd, waarbij zij zowel een gepubliceerde MaxSAT-formulering als de commerciële solver Gurobi overtreffen in oplossefficiëntie.

Oorspronkelijke auteurs: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Gepubliceerd 2026-08-04

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je de ultieme feestplanner bent voor een enorme, prestigieuze zakelijke conventie. Je hebt honderden mensen die één-op-één gesprekken moeten voeren, maar iedereen heeft verschillende schema's, sommige kamers zijn piepklein terwijl andere enorm groot zijn, en bepaalde vergaderingen moeten plaatsvinden voordat andere kunnen beginnen. Je doel is niet alleen om iedereen een afspraak te geven; het is om ervoor te zorgen dat niemand te lang saai rondzit tussen zijn of haar afspraken door. Dit is de chaotische puzzel van "Business-to-Business (B2B) meeting scheduling."

Om dit op te lossen, gebruiken informaticus een speciaal soort logisch spel genaamd SAT (Satisfiability). Denk aan SAT als een superintelligente detective die controleert of een reeks regels ooit tegelijkertijd waar kan zijn. Als je de detective vertelt: "Vergadering A moet vóór Vergadering B plaatsvinden, maar Vergadering B moet vóór Vergadering A plaatsvinden," zegt de detective direct: "Onmogelijk!" Maar als de regels lastig maar mogelijk zijn, vindt de detective een geldig schema. Een andere versie, MaxSAT, is als een detective die niet alleen een geldig schema vindt, maar ook probeert het perfect te maken door te minimaliseren hoeveel tijd mensen moeten wachten tussen hun afspraken. Deze paper duikt in hoe we deze logische detectives sneller en slimmer kunnen maken bij het organiseren van deze complexe zakelijke evenementen.

Het Probleem: Een Verstrengeld Web van Vergaderingen

In de wereld van zakelijke vergaderingen wordt het snel rommelig. Je hebt een lijst met vergaderingen, een lijst met tijdsloten en een lijst met kamers. De regels zijn strikt:

Geen Overlap: Een persoon kan niet op twee plaatsen tegelijk zijn.
Kamercapaciteit: Een kamer kan niet meer vergaderingen huisvesten dan de capaciteit toelaat.
Precedentie: Sommige vergaderingen moeten plaatsvinden vóór andere (zoals een ochtendbriefing vóór een middagworkshop).
Het "Idle"-probleem: Het echte hoofdpijndossier is "idle time" (wachttijd). Als een deelnemer een vergadering heeft om 9:00 uur en de volgende pas om 11:00 uur, dan heeft diegene twee uur aan "idle time". Het doel van dit onderzoek is om dit te balanceren, zodat niemand urenlang zit te wachten terwijl anderen slechts enkele minuten wachten. Het gaat om eerlijkheid en efficiëntie.

De Oude Manier versus de Nieuwe Manier

De onderzoekers keken naar een bestaande methode (genaamd ORG-MAXSAT) die al behoorlijk goed was. Echter, ze merkten op dat het was alsof je een feest probeerde te organiseren door elke mogelijke combinatie van gasten en tijden op te schrijven, zelfs de combinaties die overduidelijk onmogelijk waren. Het was lomp, traag en verbruikte veel computergeheugen.

Het team van de VNU University of Engineering and Technology in Vietnam besloot een "compacte" versie te bouwen. Ze introduceerden drie belangrijke trucs om het probleem te verkleinen:

De "Pre-Check" Filter (Domain Filtering): Voordat ze de computerdetective überhaupt om de puzzel vragen, voegden ze een slimme filter toe. Deze filter bekijkt de regels en kruist direct onmogelijke opties door. Bijvoorbeeld: als een vergadering moet plaatsvinden na een andere vergadering die om 14:00 uur eindigt, verwijdert de filter onmiddellijk alle tijdsloten vóór 14:00 uur uit de lijst met mogelijkheden. Dit is als het opruimen van de rommel van een bureau voordat je probeert een specifieke pen te vinden. Ze bewezen dat deze filter nooit een geldige oplossing weggooit; het verwijdert alleen de troep.
De "Gedeelde Trap" (Sparse Shared-Suffix Encoding): Wanneer men te maken krijgt met de "moet plaatsvinden vóór"-regels, schreef de oude methode een aparte notitie voor elk enkel paar vergaderingen. Als je 100 vergaderingen had, waren dat duizenden notities. De nieuwe methode merkte op dat veel van deze notities hetzelfde zeiden. In plaats van apart te schrijven "Vergadering A vóór B", "Vergadering A vóór C" en "Vergadering A vóór D", creëerden ze een gedeelde "trap" van logica. Ze hergebruiken variabelen voor vergelijkbare situaties, zoals het gebruik van één meester sleutel voor meerdere deuren in plaats van een nieuwe sleutel te maken voor elk afzonderlijk slot.
De "Fairness" Score (Idle-Time Balancing): In plaats van alleen het aantal pauzes te tellen, creëerden ze een nieuwe manier om "idle time" te meten. Ze keken naar de tijd tussen de eerste en de laatste vergadering van een persoon. Als iemand vergaderingen heeft om 9:00 en 11:00, dan is de "span" (het bereik) twee uur. Als iemand slechts één vergadering heeft, is er nul "idle time". Het doel is om de difference tussen de idle time van de meest bezette persoon en de idle time van de minst bezette persoon zo klein mogelijk te maken.

Wat Ze Hebben Gevonden

De onderzoekers testten hun nieuwe "Compacte" methode tegen de oude methode en tegen enkele zeer krachtige commerciële softwarepakketten (zoals Gurobi en CPLEX) op 126 officiële testgevallen en 100 extra "stress-test" gevallen met nog meer vergaderingen.

Hier zijn de resultaten, die behoorlijk indrukwekkend zijn:

Kleinere Omvang: De nieuwe methode verminderde het aantal logische "clauses" (de regels die de computer moet controleren) met gemiddeld 40,3%.
Minder Geheugen: Het gebruikte 55,9% minder piekgeheugen. Stel je voor dat je de helft van de RAM nodig hebt om hetzelfde puzzel op te lossen.
Hogere Snelheid: De totale tijd om de problemen op te lossen daalde met 14,0%.
De Kracht van Filtering: Alleen al het gebruik van de "Pre-Check" filter verminderde het aantal variabelen met 24,1% en de regels met 16,2%.
De Kracht van Delen: De "Shared Staircase"-truc sneed nog eens 0,5% tot 5,5% van de regels weg, afhankelijk van hoe druk het schema was.

Het Oordeel

Het meest opwindende deel is dat hun nieuwe compacte SAT- en MaxSAT-methoden in staat waren om elk één van de 126 officiële testgevallen op te lossen. Nog beter: ze deden het sneller dan de toonaangevende commerciële solver, Gurobi, in termen van de mediaan tijd. Terwijl andere commerciële tools (zoals CPLEX en CP Optimizer) moeite hadden om alle gevallen binnen de tijdslimiet op te lossen, handte de nieuwe SAT-gebaseerde aanpak ze allemaal af.

De paper beweert niet dat ze de problemen met het plannen van het universum voor altijd hebben opgelost, maar het heeft zeker aangetoond dat door de regels op te schonen en het werk slimmer te delen, we computers veel beter kunnen maken in het organiseren van ons drukke leven. Het verandert een enorme, verstrengelde knoop van vergaderingen in een net, gebalanceerd schema waarbij iedereen een eerlijk deel van de tijd krijgt en niemand te lang in de gang hoeft te wachten.

Technische Samenvatting: Compacte SAT- en MaxSAT-coderingen voor B2B-vergaderplanning met evenwichtige inactiviteitstijden

Probleemdefinitie

Het artikel behandelt B2B-vergaderplanning (Business-to-Business), een combinatorisch optimalisatieprobleem waarbij gevraagde tweezijdige vergaderingen aan specifieke tijdsloten en locaties moeten worden toegewezen. De planning moet voldoen aan verschillende beperkingen:

Niet-overlap van deelnemers: Een deelnemer kan niet gelijktijdig aan twee vergaderingen deelnemen.
Locatiecapaciteit: Het aantal vergaderingen in een tijdslot mag de beschikbare capaciteit aan locaties ( $K$ ) niet overschrijden.
Beschikbaarheid & Beperkingen: Vergaderingen moeten plaatsvinden binnen gevraagde sessies, vaste slots of verboden slots.
Precedentie: Gerichte bogen $(i, j)$ dwingen af dat vergadering $i$ vóór vergadering $j$ moet plaatsvinden.

Het doel dat in dit werk wordt voorgesteld, verschilt van eerdere formuleringen (die vaak "break groups" minimaliseren of de discrepantie in het aantal pauzes begrenzen). In plaats daarvan minimaliseert deze studie de range van de interne inactiviteits-slot-totalen ( $\Delta I$ ) onder deelnemers met ten minste twee vergaderingen. Interne inactiviteits-slots worden gedefinieerd als onbezette tijd strikt tussen de eerste en laatste toegewezen vergadering van een deelnemer. Deze metriek maakt onderscheid tussen korte onderbrekingen en langere wachttijden, met als doel een gebalanceerde lastverdeling die vergelijkbaar is met het Balanced Academic Curriculum Problem (BACP). Een geaggregeerde maatstaf voor inactiviteit ( $I_\Sigma$ ) wordt ook gerapporteerd als een complementaire metriek.

Methodologie

De auteurs stellen een compacte SAT (Boolean Satisfiability) en MaxSAT codering voor die drie primaire modelleringverbeteringen integreert ten opzichte van bestaande gepubliceerde formuleringen:

Oplossingsbehoudende Domeinfiltering (Preprocessing):
Voordat de Conjunctive Normal Form (CNF) wordt gegenereerd, passen de auteurs een preprocessing-algoritme toe (Algoritme 1) dat niet-ondersteunde toewijzingen verwijdert. Dit integreert:
- Endpoint-bound filters: Propagatie van precedentiebeperkingen langs paden (met gebruik van directe bogen of transitieve afsluiting).
- Per-deelnemer matching: Het verwijderen van toewijzingen die geen deel kunnen uitmaken van een conflictvrije planning voor een specifieke deelnemer.
- Saturated-slot propagatie: Het elimineren van slots waar de capaciteit al volledig bezet is door gedwongen toewijzingen.
- Claim: Dit proces behoudt alle haalbare schema's terwijl het domeingrootte vermindert, waardoor het aantal variabelen en clausules wordt gereduceerd.
Sparse Shared-Suffix Precedence Encoding (SPARSESUFFIX):
In plaats van precedentierelaties te coderen met behulp van paarwijze clausules (wat kwadratisch kan zijn in domeingrootte), introduceren de auteurs een ijle (sparse) codering.
- Het materialiseert alleen de onderscheidende "cut points" in het predecessor-domein waar de beperking actief wordt.
- Het hergebruikt hulpvariabelen voor gelijke sneden over verschillende relaties heen.
- Er is bewezen dat deze aanpak equivalent is aan paarwijze clausules, maar het vermindert het aantal clausules aanzienlijk, vooral in combinatie met domeinreductie.
Range-gebaseerde Inactiviteitstijd-doelstelling:
Het paper introduceert een exacte codering om de range van interne inactiviteits-slots ( $\Delta I$ ) te minimaliseren.
- Het afleiden van de eerste en laatste bezette slots voor elke deelnemer.
- Het gebruikt een lineair aantal hulpvariabelen om het verschil tussen de maximale en minimale inactiviteitstotalen over alle relevante deelnemers te berekenen.

De studie evalueert deze componenten tegenover een baseline ORG-MAXSAT formulering (een adaptatie van een gepubliceerd model) en commerciële solvers (Gurobi, CPLEX, CP Optimizer). De evaluatie beslaat 126 officiële benchmark-instanties en 100 afgeleide "Stress"-instanties met variërende precedentiedichtheid.

Belangrijkste Bijdragen

Het paper identificeert drie specifieke bijdragen:

Preprocessing Procedure: Een filterintegratie die niet-ondersteunde toewijzingen verwijdert vóór de CNF-generatie. Propositie 1 bewijst dat dit de haalbaarheid behoudt, en empirische resultaten tonen aan dat het de toewijzingsvariabelen met 24,1% en de clausules met 16,2% vermindert.
Sparse Shared-Suffix Representatie: Een exacte codering (SPARSESUFFIX) die alleen vereiste predecessor-domein cut points materialiseert. Propositie 3 bewijst de equivalentie met paarwijze clausules. De studie laat zien dat hoewel domeinreductie het aantal variabelen verlaagt, suffix-sharing onafhankelijk het aantal clausules verlaagt.
B2B-Specifieke Doelstelling: Een range-gebaseerde inactiviteitstijd-doelstelling die de discrepantie in interne wachttijden meet, gecodeerd met een lineair aantal hulpvariabelen.

Experimentele Resultaten

De experimenten werden uitgevoerd op een 4-core machine met een tijdlimiet van 7.200 seconden. Belangrijkste bevindingen zijn:

Formulegrootte en Geheugen: Vergeleken met de aangepaste ORG-MAXSAT baseline, reduceerde de voorgestelde compacte codering het mediane aantal clausules met 40,3% en het mediane piekgeheugengebruik met 55,9%.
Impact van Domeinreductie: Domeinfiltering alleen al verminderde de toewijzingsvariabelen met 24,1% en de clausules met 16,2%, wat het grootste deel van de reductie in formulegrootte verklaart.
Precedentie-codering: De SPARSESUFFIX-codering verminderde het mediane aantal clausules met 0,5%–1,0% op officiële precedentie-instanties en tot wel 5,5% op de meest dichtbevolkte afgeleide instanties (wanneer gecombineerd met transitieve afsluiting).
Solver Prestaties:
- Alle drie de voorgestelde SAT/MaxSAT methoden (Incremental SAT, Non-Incremental SAT, en UWrMaxSAT) losten alle 126 officiële instanties op.
- Vergeleken met Gurobi (de enige commerciële solver die alle instanties oploste), behaalden de voorgestelde SAT/MaxSAT methoden een lagere mediane totale tijd.
- Incremental SAT behaalde de laagste mediane tijd (0,227s) onder de volledige methoden.
- CP Optimizer had de laagste mediane tijd (0,110s) maar slaagde er niet in om 11 instanties binnen de tijdlimiet op te lossen.

Betekenis en Claims

Het paper claimt dat de voorgestelde compacte codering een significante efficiëntieverbetering biedt ten opzichte van bestaande Boolean formuleringen voor B2B-vergaderplanning. Door domeinfiltering te scheiden van de precedentie-representatie, laten de auteurs zien dat domeinreductie de primaire drijfveer is voor het verminderen van de formulegrootte, terwijl sparse shared-suffix codering aanvullende clausereductie biedt, onafhankelijk van de relatieset.

De studie stelt dat de nieuwe inactiviteitstijd-range doelstelling een meer genuanceerde maatstaf voor de kwaliteit van de planning biedt dan eerdere "break group" metrieken, door onderscheid te maken tussen korte onderbrekingen en lange wachttijden. Voorts geven de resultaten aan dat moderne SAT en MaxSAT solvers, wanneer zij zijn uitgerust met deze compacte coderingen, de leidende commerciële MIP en CP solvers kunnen overtreffen in termen van mediane oplossingstijd voor deze specifieke probleemklasse, waarbij zij alle benchmark-instanties oplossen waar sommige commerciële solvers de tijdlimiet overschreden.

De auteurs blijven bescheiden over toekomstig werk, waarbij zij opmerken dat de huidige studie zich richt op single-run timing en dat toekomstig onderzoek herhaalde timing-runs en lexicografische doelstellingen (het minimaliseren van $\Delta I$ vóór $I_\Sigma$ ) zou kunnen verkennen.