💻 computer science

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

Questo lavoro presenta un framework basato su SAT e MaxSAT per risolvere il problema di taglio bidimensionale con un unico formato di scorta, che, grazie a tecniche come l'eliminazione delle orientazioni non ammissibili e diverse strategie di ottimizzazione, supera significativamente le prestazioni di strumenti commerciali come OR-Tools, CPLEX e Gurobi su benchmark standard.

Autori originali: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Pubblicato 2026-04-03

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di essere un maestro falegname o un tagliatore di stoffa. Hai un enorme magazzino di fogli di legno o di tessuto tutti uguali (le "lastre") e una lista lunghissima di pezzi da tagliare: alcuni sono piccoli quadrati, altri lunghi rettangoli. Il tuo obiettivo è semplice ma insidioso: tagliare tutti i pezzi richiesti usando il minor numero possibile di fogli, per non sprecare materiale e risparmiare soldi.

Questo è il problema che gli autori di questo articolo, Tuyen, Chi e Khanh, hanno deciso di risolvere con un approccio matematico molto intelligente. Ecco la loro storia raccontata in modo semplice.

Il Problema: Il Caos dei Tagli

Il problema si chiama Cutting Stock Problem (Problema del Taglio delle Lastre). È come se dovessi riempire dei contenitori (i fogli) con oggetti di forme diverse.
La difficoltà non è solo nel trovare un posto per ogni pezzo, ma nel fatto che devi fare molte copie dello stesso pezzo. Se ti servono 20 pezzi di un certo tipo, devi trovare un posto per tutti e 20, e non possono sovrapporsi. Più pezzi hai, più il numero di combinazioni possibili esplode, rendendo il calcolo quasi impossibile per i computer tradizionali.

La Soluzione: I "Detective Logici" (SAT e MaxSAT)

Gli autori hanno detto: "Dimentichiamo i metodi tradizionali di calcolo. Usiamo invece la logica booleana (SAT)".
Immagina il computer non come un calcolatore veloce, ma come un detective super-organizzato.

Il Detective (SAT): Il detective ha una lista di regole rigide: "Se metto questo pezzo qui, non posso mettere quello lì". Il suo compito è provare a disporre i pezzi su un foglio. Se ci riesce, grida "SOLUZIONE TROVATA!". Se non ci riesce, grida "IMPOSSIBILE!" e ricorda perché non è riuscito (questa è la parte magica: impara dagli errori).
La Strategia (MaxSAT): A volte il detective non deve solo trovare una soluzione, ma la migliore (quella che usa meno fogli). Per farlo, usa una versione avanzata (MaxSAT) che cerca di massimizzare il risparmio.

Le Tre Strategie di Gioco

Gli autori hanno provato tre modi diversi per far lavorare il detective:

Il Metodo "Ricomincia da Zero" (Non-Incremental SAT):
Immagina di chiedere al detective: "Riesci a mettere tutto su 5 fogli?". Se dice di no, tu gli chiedi: "E su 6?". Ogni volta, gli dai un foglio bianco pulito. È semplice, ma se il detective ha già imparato che "tre pezzi grandi non stanno mai insieme", deve riscoprirlo ogni volta. È come studiare per un esame ripassando tutto da capo ogni giorno.
Il Metodo "Memoria a Lungo Termine" (Incremental SAT):
Qui il detective è più furbo. Gli dici: "Prova con 5 fogli". Se fallisce, lui ti dice "No, non ci stanno". Poi, invece di cancellare la lavagna, gli dici: "Ok, prova con 6 fogli, ma ricorda che i tre pezzi grandi non stanno insieme". Il detective ricorda tutto ciò che ha imparato prima. È come se avesse un quaderno degli appunti dove scrive le regole che ha scoperto. Questo funziona benissimo quando i pezzi sono tutti dritti (senza rotazione).
Il Metodo "Tutto in Una Volta" (MaxSAT):
Invece di chiedere "5? 6? 7?", dai al detective un foglio unico con scritto: "Trova il modo migliore per usare meno fogli possibili, ma non superare il limite massimo". È potente, ma a volte il detective si perde nei dettagli e impiega troppo tempo a decidere.

La Magia della Rotazione

C'è un dettaglio fondamentale: i pezzi possono essere ruotati?

Senza rotazione: I pezzi sono come mattoni che vanno solo in orizzontale. Qui il metodo "Memoria a Lungo Termine" (Incremental) vince a mani basse perché le regole che impara sono molto utili e riutilizzabili.
Con rotazione: I pezzi possono girare di 90 gradi (come un libro che puoi tenere in verticale o orizzontale). Questo raddoppia le possibilità di confusione. In questo caso, il metodo "Ricomincia da Zero" (Non-Incremental) funziona meglio perché la memoria del detective diventa troppo pesante e piena di informazioni inutili. Meglio ripartire fresco ogni volta.

Il Risultato: Chi ha vinto?

Gli autori hanno messo alla prova il loro sistema contro i giganti del settore (software commerciali come OR-Tools, CPLEX e Gurobi) usando una lista di 30 problemi difficili.

Il risultato è stato sorprendente:

I loro "detective logici" sono riusciti a dimostrare che una soluzione era perfetta e ottimale (cioè non esisteva un modo migliore) in due o tre volte più casi rispetto ai software commerciali.
Quando non riuscivano a trovare la soluzione perfetta, si avvicinavano molto di più al risultato ideale rispetto ai concorrenti.
In pratica, il loro metodo ha trovato soluzioni migliori e ha dimostrato matematicamente che erano le migliori, molto più spesso degli altri.

In Sintesi

Questo articolo ci dice che, invece di usare i soliti metodi di calcolo pesante per problemi di taglio e impacchettamento, possiamo usare la logica pura e la memoria intelligente dei computer.
È come se avessimo scoperto che, invece di spingere un macigno con la forza bruta (i metodi tradizionali), possiamo usare un sistema di leve e ingranaggi (la logica SAT) che, se usato nel modo giusto (a seconda se si può ruotare o meno), fa il lavoro con meno fatica e con risultati superiori.

È una vittoria della "intelligenza logica" sulla "forza di calcolo grezza".

1. Il Problema: 2D-CSSP

Il lavoro si concentra sul Problema di Taglio di Stock Unico Bidimensionale (2D-CSSP).

Definizione: L'obiettivo è tagliare un insieme di pezzi rettangolari (con dimensioni e richieste specifiche) da fogli di materiale grezzo identici, minimizzando il numero totale di fogli utilizzati.
Complessità: A differenza del classico problema di Bin Packing (dove ogni oggetto è unico), il 2D-CSSP richiede di soddisfare la domanda ( $d_t \ge 1$ ) per ogni tipo di oggetto. Questo introduce una "esplosione combinatoria" significativa, poiché ogni tipo di oggetto viene replicato $d_t$ volte, moltiplicando lo spazio di ricerca.
Vincoli: Gli oggetti devono essere posizionati senza sovrapposizioni all'interno dei fogli, rispettando i limiti dimensionali. È consentita la rotazione di 90 gradi.
Gap nella letteratura: I metodi esatti esistenti (come la generazione di colonne o i modelli MIP) faticano a scalare con domande elevate a causa della crescita esponenziale delle variabili geometriche. I metodi euristici sono veloci ma non forniscono certificati di ottimalità. Non esisteva finora una formulazione basata sulla logica booleana (SAT) specifica per questo problema.

2. Metodologia e Codifica SAT

Gli autori propongono un framework basato su SAT (Boolean Satisfiability) e MaxSAT per risolvere il problema in modo esatto.

Codifica Proposizionale

Il cuore della metodologia è una codifica efficiente che gestisce la struttura della domanda:

Espansione della Domanda: I tipi di oggetti vengono espansi in singole copie ( $c_{t,1}, \dots, c_{t,d_t}$ ).
Variabili di Assegnazione: Ogni copia ha una variabile booleana che indica a quale foglio ( $j$ ) è assegnata.
Vincoli di Non-Sovrapposizione Condizionali: Questa è l'innovazione chiave. I vincoli di non-sovrapposizione tra due copie $c$ $c$ e $c'$ $c^{'}$ sono attivati solo se entrambe sono assegnate allo stesso foglio.
- Logica: $\neg s_{c,j} \lor \neg s_{c',j} \lor \text{non-overlap}(c, c')$ .
- Questo evita di generare vincoli geometrici inutili tra oggetti su fogli diversi, mantenendo la formula più compatta.
Codifica dell'Ordine: Le coordinate $(x, y)$ sono codificate usando un approccio "order encoding" (variabili booleane che rappresentano $x \le e$ ), che mantiene il numero di variabili lineare rispetto alle dimensioni del foglio.
Simmetria e Rotazione:
- Eliminazione della Simmetria: Vengono applicate regole per rompere le simmetrie indotte dalla domanda (es. ordinare copie dello stesso tipo) e per l'ordinamento dei fogli (i fogli vengono usati in ordine di indice).
- Regola di Eliminazione Orientazione Non Fattibile: Se un oggetto può adattarsi al foglio solo in un'orientazione (o non si adatta affatto), la variabile di rotazione viene fissata tramite una clausola unitaria, riducendo lo spazio di ricerca.

Strategie di Risoluzione

Vengono confrontati tre approcci per trovare il numero minimo di fogli ( $k$ ):

SAT Non Incrementale con Ricerca Binaria: Si costruisce una nuova formula per ogni valore di $k$ testato. Ogni iterazione è indipendente.
SAT Incrementale con Ricerca Binaria: Si costruisce una volta sola la formula per il limite superiore di fogli. Per testare un numero inferiore $m$ , si usano "assunzioni" per disattivare i fogli extra. I conflitti (clausole apprese) derivanti da tentativi falliti con $m$ fogli vengono riutilizzati quando si prova con $m+1$ fogli.
MaxSAT Parziale Ponderato: L'obiettivo di minimizzare i fogli è codificato direttamente come un insieme di clausole "soft" (da massimizzare il numero di fogli non usati) all'interno di una singola chiamata al solver, evitando la ricerca binaria.

3. Contributi Chiave

Prima codifica SAT per 2D-CSSP: Un approccio che gestisce nativamente la replicazione degli oggetti e i vincoli condizionali di non-sovrapposizione.
Regola di fissaggio dell'orientazione: Un'estensione generale delle regole di simmetria che fissa la rotazione quando geometricamente obbligata.
Analisi dell'interazione Domanda-SAT: Dimostrazione che la struttura della domanda (copie identiche) permette un trasferimento efficace delle clausole apprese tra iterazioni nel caso incrementale, un fenomeno non presente nel Bin Packing standard.
Benchmark Estensivo: Confronto su larga scala (30 istanze Cui-Zhao) contro solver commerciali (OR-Tools, CPLEX, Gurobi).

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un set di benchmark Cui-Zhao (30 istanze, da 7 a 21 tipi di oggetti, domande fino a 45).

Performance Assoluta:
- Le configurazioni SAT basate su questo framework hanno certificato l'ottimalità per 2-3 volte più istanze rispetto ai migliori solver commerciali (16-18 istanze certificate contro 1-7 per OR-Tools/CPLEX/Gurobi).
- Il gap di ottimalità (differenza tra la soluzione trovata e il limite inferiore noto) è significativamente inferiore rispetto ai metodi MIP e CP commerciali.
Confronto tra Strategie SAT:
- Senza Rotazione: L'approccio Incrementale SAT è superiore. Le clausole apprese durante i tentativi falliti su $k$ fogli sono valide e utili anche per $k+1$ fogli grazie alla struttura delle copie identiche.
- Con Rotazione: L'approccio Non-Incrementale SAT diventa più efficace. La rotazione aumenta drasticamente il numero di clausole (esplosione combinatoria), rendendo il database di clausole apprese troppo grande e "rumoroso" per l'approccio incrementale. In questo caso, ricominciare da zero con una formula più piccola (ma specifica per quel $k$ ) funziona meglio.
Confronto con Solver Commerciali:
- OR-Tools (CP-SAT): È il miglior solver commerciale, spesso trovando soluzioni vicine all'ottimo, ma fallisce nel certificare l'ottimalità per la maggior parte delle istanze.
- CPLEX e Gurobi (MIP): Faticano a risolvere istanze di dimensioni moderate entro i limiti di tempo, mostrando gap elevati e pochi certificati di ottimalità.
- Vantaggio SAT: Il meccanismo di prova CDCL (Conflict-Driven Clause Learning) dei solver SAT fornisce certificati di ottimalità molto più robusti rispetto ai metodi basati su rilassamenti lineari o vincoli globali standard.

5. Significato e Conclusioni

Questo lavoro dimostra che i metodi basati sulla logica booleana (SAT/MaxSAT) sono competitivi, e spesso superiori, ai metodi di programmazione matematica tradizionali per problemi di taglio e impaccamento con domande elevate.

Impatto Teorico: Colma il divario tra la teoria della soddisfacibilità booleana e i problemi pratici di produzione industriale, mostrando come la struttura specifica del problema (domanda multipla) possa essere sfruttata per ottimizzare la risoluzione.
Impatto Pratico: Offre un'alternativa potente per l'industria manifatturiera (acciaio, vetro, tessuti) dove la garanzia di ottimalità è cruciale per ridurre gli scarti e i costi.
Direzioni Future: Gli autori suggeriscono l'integrazione con la generazione di colonne (usando SAT per il sottoproblema di pricing) e l'estensione a varianti con dimensioni di stock eterogenee.

In sintesi, il paper stabilisce un nuovo stato dell'arte per il 2D-CSSP, dimostrando che un'attenta codifica SAT combinata con strategie di risoluzione adattive (incrementale vs non incrementale a seconda della rotazione) supera le capacità dei solver industriali attuali.