Accelerating Discrete Facility Layout Optimization: A Hybrid CDCL and CP-SAT Architecture

Technische Samenvatting: Conflict-Driven Clause Learning met VSIDS-heuristieken voor Discrete Inrichtingsplanning

Probleemdefinitie
Het artikel behandelt het Discrete Facility Layout Problem (FLP), met name gericht op roostergebaseerde indelingen waarbij machines moeten worden toegewezen aan plekken onder dichte combinatorische beperkingen. Deze beperkingen omvatten een-op-een toewijzing, nabijheidseisen (moeten buren zijn), scheidingsbeperkingen (verboden buren), geblokkeerde cellen (gangen) en toewijzing over meerdere verdiepingen. Waar canonieke formuleringen het FLP vaak behandelen als een Quadratic Assignment Problem (QAP), introduceren realistische gevallen logisch zware beperkingen die een dichte combinatorische structuur creëren. De studie onderzoekt of moderne SAT-oplossers die Conflict-Driven Clause Learning (CDCL) gebruiken met de Variable State Independent Decaying Sum (VSIDS)-heuristiek, deze structuur effectief kunnen benutten, en onder welke voorwaarden ze gunstig kunnen concurreren met gevestigde Constraint Programming (CP-SAT) en Mixed-Integer Linear Programming (MILP) benaderingen.

Methodologie
De auteurs ontwikkelden een geünificeerde benchmarkomgeving in Python om gecontroleerde vergelijkingen uit te voeren tussen drie oplossingsparadigma's:

1. CDCL+VSIDS: Geïmplementeerd met PySAT met Glucose4 en MiniSat22 als back-ends. De haalbaarheid van de indeling is gecodeerd in Conjunctive Normal Form (CNF) met Booleaanse variabelen ($z_{ij}$) voor machine-plek-toewijzingen. Beperkingen zijn gecodeerd via kardinaliteitsbeperkingen (met sequentiële tellers of totalizers om het aantal clauses te verminderen), nabijheids-/scheidingsclauses en unit-clauses voor geblokkeerde cellen. Optimalisatie wordt afgehandeld door CDCL te behandelen als een haalbaarheidsengine, terwijl optimalisatiedoelstellingen worden aangepakt via hybride architecturen.
2. CP-SAT: Geïmplementeerd via Google OR-Tools, met gebruikmaking van globale beperkingen en pseudo-Booleaanse redenering.
3. MILP: Geïmplementeerd via PuLP met CBC, met gebruikmaking van gelineariseerde QAP-formuleringen.

Experimenteel Ontwerp
De studie gebruikte synthetische data om algoritmische prestaties te isoleren van real-world variatie. Experimenten varieerden in:

• Roostergroottes: Variërend van 2×2 tot 6×6 (met 5×5 als drempel voor MILP-falen en 6×6 als limiettest voor onoplosbaarheid).
• Beperkingdichtheid ($\rho$): Variërend van 0,05 tot 0,35.
• Structurele Typen: Alleen toewijzing, met nabijheidsbeperkingen, met scheidingsbeperkingen en gemengd.
• Symmetrie: Tests werden uitgevoerd met en zonder positiestelling van de eerste machine om symmetrie te doorbreken.
• Time-outs: 10 seconden voor haalbaarheidscontroles en 60 seconden voor optimalisatietests.

Belangrijkste Bevindingen

• Haalbaarheidsdetectie: CDCL+VSIDS vertoont een bijna constante runtime-prestatie over variërende roostergroottes en beperkingdichtheden heen, en presteert beter dan CP-SAT met een factor van tien tot honderd en beter dan MILP met nog grotere marges. CDCL blinkt uit in het afsnijden van de zoekruimte voor pure haalbaarheid.
• Optimalisatie: Hoewel CDCL snel is in het vinden van een oplossing, kan het op zichzelf geen zachte doelstellingen optimaliseren (zoals het minimaliseren van de Manhattan-afstand) zonder MaxSAT of iteratieve verkrapping van grenswaarden, wat overhead toevoegt. CP-SAT blinkt uit in hybride logisch-numerieke optimalisatie, en bewijst globale optima voor 5×5 en 6×6 gevallen waar MILP niet binnen de tijdslimiet convergeerde.
• MILP-beperkingen: MILP vertoont een exponentiële vertraging naarmate de roostergrootte en beperkingdichtheid toenemen, met moeite door de zwakke lineaire relaxaties veroorzaakt door big-M disjuncties en dichte paarsgewijze termen.
• Symmetriebreking: Het vaststellen van de positie van een machine verbeterde de runtime van CP-SAT (27%) en MILP (50%) aanzienlijk, maar veroorzaakte een lichte vertraging voor CDCL, omdat de toegevoegde clauses de complexiteit van de formule verhoogden zonder dezelfde afsnijdbaten te bieden in een clause-learning context.

Hybride Architecturen
Om de snelheid van CDCL en de optimalisatiekwaliteit van CP-SAT te benutten, stelden de auteurs twee hybride architecturen voor:

1. Diepe Enumeratie (Architectuur A): CDCL enumerateert een groot aantal haalbare indelingen (75.000 samples), en CP-SAT selecteert de beste. Deze aanpak vond een levensvatbare oplossing (Obj=22,0) in ~24 seconden, aanzienlijk sneller dan de 60-seconden CP-SAT-baseline, hoewel het niet het globale optimum bereikte (Obj=13,0).
2. Warm-Start (Architectuur B): CDCL genereert een enkele snelle haalbare hint (een bovengrens) en injecteert deze in het branch-and-bound-proces van CP-SAT. Deze aanpak bereikte het globale optimum (Obj=13,0) met een gevalideerde runtime-voorsprong ten opzichte van de cold-start baseline, wat aantoont dat CDCL-gedreven hints effectief de initiële takken van de zoekboom afsnijden.

Betekenis en Claims
Het artikel beweert dat de meest effectieve weg voor discrete inrichtingsplanning niet ligt in het vervangen van exacte oplossers, maar in het versnellen ervan met behulp van CDCL-gedreven haalbaarheidshints. De studie stelt vast dat:

• CDCL+VSIDS een "ongekende dominantie" bezit in pure haalbaarheidsdetectie voor logisch zware, roostergebaseerde FLP's, waarbij complexe nabijheids- en scheidingsregels met een factor van tien tot honderd sneller worden opgelost dan met CP-SAT of MILP.
• Pure CDCL worstelt met kostenbewuste optimalisatie, waardoor het ongeschikt is als een zelfstandige optimizer voor deze problemen.
• Hybride architecturen, specifiek de Warm-Start-aanpak, slaan succesvol de brug tussen snelle vervulbaarheid en bewezen optimaliteit. Door CDCL te gebruiken om een geldige bovengrens te bieden, bereikt het hybride systeem globale optima met gevalideerde algoritmische snelheidsvoordelen ten opzichte van cold-start baselines.

De auteurs concluderen dat hoewel CDCL zelden wordt toegepast op volledige fabrieks-FLP's vanwege optimalisatiemismatches en coderings- overhead, de integratie ervan als haalbaarheidsengine binnen een hybride raamwerk een robuuste oplossing biedt voor inrichtingsproblemen met hoge complexiteit.