Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT

Titel: Oplossen van het Tweedimensionale Single Stock Size Cutting Stock Probleem met SAT en MaxSAT

Auteurs: Tuyen Van Kieu, Chi Linh Hoang en Khanh Van To (VNU University of Engineering and Technology, Hanoi, Vietnam)

---

1. Probleemdefinitie

Het artikel richt zich op het Tweedimensionale Single Stock Size Cutting Stock Problem (2D-CSSP). Dit is een klassiek productieprobleem waarbij rechthoekige items moeten worden uitgesneden uit identieke voorraadbladen (sheets) om aan specifieke vraag (demand) te voldoen, terwijl het aantal benodigde bladen wordt geminimaliseerd.

• Kerncomplexiteit: Het probleem generaliseert het Tweedimensionale Bin Packing Probleem (2D-BPP). Het onderscheidende kenmerk is dat er meerdere exemplaren ($d_t \ge 1$) van elk itemtype $t$ nodig zijn.
• Uitdaging: Deze vraagvermenigvuldiging leidt tot een sterke combinatorische explosie. Als een type $d_t$ exemplaren heeft, moet het model beslissen over de toewijzing van elk individueel exemplaar aan een blad, hun positie en rotatie, en de niet-overlappende constraints tussen alle paren op hetzelfde blad.
• Doel: Het vinden van een toewijzing en plaatsing voor alle $N = \sum d_t$ exemplaren op een minimaal aantal $k$ bladen, zodat geen overlap optreedt en alle items binnen de bladgrenzen blijven.

2. Methodologie en Encoding

De auteurs presenteren een nieuw raamwerk gebaseerd op Boolean Satisfiability (SAT) en MaxSAT. In tegenstelling tot traditionele MIP- of CP-aanpakken, gebruiken ze een logische encoding die specifiek is ontworpen voor de vraagstructuur.

A. SAT-encoding

De encoding vertaalt het geometrische probleem naar een propositional formule $\Phi_k$ voor een vast aantal bladen $k$:

• Variabelen:
  • Bladtoewijzing: Variabelen $s_{c,j}$ geven aan of kopie $c$ op blad $j$ ligt.
  • Positie: Gebruik van order encoding voor de coördinaten $(x_c, y_c)$. Dit vertegenwoordigt integer variabelen met een lineair aantal booleaanse variabelen, wat de encoding compact houdt.
  • Rotatie: Een variabele $r_c$ bepaalt of een item 90 graden is gedraaid.
• Conditionele Niet-overlap Constraints:
  • Dit is de kerninnovatie. In plaats van niet-overlap te forceren voor alle paren, worden deze constraints conditioneel gemaakt op basis van de bladtoewijzing.
  • Formule: $\neg s_{c,j} \lor \neg s_{c',j} \lor \text{niet-overlap}(c, c')$.
  • Dit betekent dat de geometrische scheiding alleen wordt afgedwongen als twee items daadwerkelijk op hetzelfde blad $j$ zijn toegewezen. Dit vermindert de complexiteit aanzienlijk ten opzichte van unconditional encodings.
• Symmetrie-breking (Symmetry Breaking):
  Om de zoekruimte te verkleinen, worden vier regels toegepast:
  1. Grote items: Als twee items in elke oriëntatie te breed zijn om naast elkaar te passen, wordt hun relatieve positie vastgezet.
  2. Gelijke items ordenen: Voor meerdere exemplaren van hetzelfde type wordt een volgorde opgelegd (bijv. exemplaar $i$ kan niet links van exemplaar $j$ liggen als $i < j$) om permutatiesymmetrie te breken.
  3. Eliminatie van onhaalbare oriëntaties: Als een item in slechts één oriëntatie in het blad past, wordt de rotatievariabele direct vastgezet (unit clause).
  4. Bladordening: Bladen worden in indexvolgorde gebruikt om herschikkingssymmetrieën tussen lege bladen te elimineren.

B. Oplossingsstrategieën

Drie benaderingen worden vergeleken om het minimale $k$ te vinden:

1. Non-incremental SAT met binair zoeken: Voor een geschat $k$ wordt de formule van nul af gebouwd en opgelost. Als het onmogelijk is, wordt $k$ verhoogd; als het mogelijk is, verlaagd.
2. Incremental SAT met binair zoeken: De formule wordt eenmalig gebouwd voor het maximale aantal bladen. Tijdens het binaire zoeken worden "supers" (bladen die niet nodig zijn) uitgeschakeld via assumptions. Cruciaal: conflictklussen (conflict clauses) die tijdens een mislukte poging met $k-1$ bladen zijn geleerd, blijven bewaard en helpen de zoektocht voor $k$ te versnellen.
3. Weighted Partial MaxSAT: Het minimaliseren van het aantal bladen wordt direct geëncodet als een soft-clause probleem. De solver probeert het aantal gebruikte bladen te minimaliseren in één enkele aanroep.

3. Belangrijkste Bijdragen

1. Eerste SAT-encoding voor 2D-CSSP: Een nieuwe encoding die vraagvermenigvuldiging expliciet modelleert door items te repliceren en conditionele niet-overlap constraints te gebruiken.
2. Infeasible-orientation eliminatie: Een algemene regel die rotatievariabelen vastzet wanneer slechts één oriëntatie fysiek mogelijk is, wat een generalisatie is van eerdere regels voor vierkante items.
3. Empirisch inzicht in vraagstructuur: Het onderzoek toont aan dat de prestatie van SAT-methoden sterk afhangt van de vraagstructuur en rotatie.
   • Zonder rotatie is Incremental SAT superieur omdat conflictklussen over identieke itemkopieën effectief worden hergebruikt.
   • Met rotatie (wat de formulegrootte vergroot) presteert Non-incremental SAT beter, omdat de grote database van irrelevante klussen in incremental SAT de zoekruimte kan vervuilen.
4. Uitgebreide benchmark: Een vergelijking met state-of-the-art industriële solvers op een standaard benchmark (Cui-Zhao).

4. Experimentele Resultaten

De auteurs testten hun methoden op 30 instances van de Cui-Zhao benchmark suite en vergeleken deze met Google OR-Tools, IBM CPLEX en Gurobi.

• Optimaliteitsbewijzen: De SAT-benadering certificeert 2 tot 3 keer meer instances als optimaal bewezen dan de beste commerciële solvers.
  • Zonder rotatie: Incremental SAT bewijst 16 instances optimaal (vs. 7 voor de beste commerciële solver).
  • Met rotatie: Non-incremental SAT bewijst 18 instances optimaal (vs. 6 voor commerciële solvers).
• Optimaliteitsgap: De SAT-methoden bereiken een aanzienlijk lagere gap (afstand tot de beste bekende oplossing) dan MIP- en CP-oplossers.
  • Met rotatie: Gap van 3,24% voor SAT vs. 4,63% voor de beste commerciële solver (OR-Tools).
• Vergelijking met Commercial Solvers:
  • OR-Tools (CP-SAT): Vond vaak oplossingen die overeenkwamen met de beste bekende oplossing (BKS), maar faalde er vaak in om de optimaliteit te bewijzen binnen de tijdslimiet.
  • CPLEX en Gurobi (MIP): Vonden vaak sneller een goede oplossing, maar faalden volledig in het bewijzen van optimaliteit voor de meeste instances en hadden hoge gaps.
• Conclusie over strategie: De keuze tussen incremental en non-incremental SAT hangt af van de formulegrootte. Incremental is krachtig bij compacte formules (geen rotatie) door hergebruik van kennis; non-incremental is robuuster bij grote formules (met rotatie).

5. Betekenis en Conclusie

Dit artikel demonstreert dat SAT-based methoden een krachtig alternatief zijn voor traditionele MIP en CP benaderingen bij complexe snijproblemen met hoge vraagvolumes.

• Technische doorbraak: De combinatie van order encoding, conditionele constraints en slimme symmetrie-breking maakt het mogelijk om de combinatorische explosie van vraagvermenigvuldiging te beheersen.
• Praktische impact: Voor industriële toepassingen betekent dit dat het mogelijk is om niet alleen goede oplossingen te vinden, maar ook wiskundig bewezen optimale oplossingen te garanderen voor problemen die voorheen als te complex werden beschouwd voor exacte methoden binnen redelijke tijdslimieten.
• Toekomst: De auteurs suggereren verdere onderzoek naar hybriden met column generation (waar SAT het pricing-subprobleem oplost) en uitbreiding naar heterogene voorraadmaten.

De broncode en benchmarkdata zijn openbaar beschikbaar gesteld, wat bijdraagt aan de reproduceerbaarheid en verdere ontwikkeling in dit domein.