💻 computer science

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

Cet article présente un cadre basé sur SAT et MaxSAT pour résoudre le problème de découpe bidimensionnelle à taille unique de stock, démontrant sur des benchmarks que cette approche surpasse les solveurs commerciaux en certifiant un nombre significativement plus élevé d'optimalités et en réduisant les écarts d'optimalité.

Auteurs originaux : Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Publié 2026-04-03

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

📦 Le Problème : Le casse-tête du déménagement géant

Imaginez que vous devez déménager. Vous avez une liste de meubles de tailles différentes (des canapés, des tables, des cartons) et une flotte de camions identiques. Votre objectif est simple : mettre tous les meubles dans le moins de camions possible sans qu'ils ne se cassent les uns contre les autres.

C'est ce qu'on appelle le "Problème de découpe bidimensionnelle" (2D-CSSP). Dans la vraie vie, cela s'applique aux usines qui découpent des plaques de verre, des tissus pour vêtements ou des tôles d'acier. Le défi, c'est que pour certains meubles (ou types de pièces), vous n'en avez pas juste un, mais des dizaines de copies (par exemple, 20 tables identiques). Cela rend le problème mathématiquement explosif, comme si vous deviez trouver l'ordre parfait pour empiler des milliers de pièces de Lego identiques.

🧠 La Solution : Le détective logique (SAT)

Les chercheurs de cet article (de l'Université d'ingénierie de Hanoï) ont décidé d'aborder ce problème non pas avec des méthodes de calcul classiques, mais avec un outil appelé SAT (Satisfaisabilité Booléenne).

Pour faire simple, imaginez que le SAT est un super-détective logique.

Au lieu de dire "essayons de placer la table ici, puis là, puis là...", le détective pose des questions binaires : "Est-ce que cette table est dans le camion 1 ? OUI ou NON".
Il utilise la logique pure pour éliminer des millions de possibilités impossibles en une fraction de seconde.

🛠️ Les Trois Astuces Magiques

Pour que ce détective soit efficace, les chercheurs ont ajouté trois règles du jeu :

La règle du "Même Camion" (Contraintes conditionnelles) :
Imaginez que vous avez 20 tables identiques. Si la table A est dans le camion 1 et la table B dans le camion 2, elles ne se gênent pas ! Le détective ne vérifie la collision que si deux tables sont dans le même camion. Cela économise énormément d'énergie de calcul.
La règle du "Tour de passe-passe" (Élimination des orientations impossibles) :
Parfois, une pièce est trop longue pour tenir à l'horizontale dans un camion, mais elle rentre parfaitement à la verticale. Le détective repère immédiatement cette situation et dit : "Pas besoin de réfléchir, cette pièce doit être tournée". Il fixe la position automatiquement, ce qui accélère la recherche.
Le détective qui se souvient (SAT Incrémental) :
C'est l'astuce la plus brillante.
- Méthode classique : Le détective essaie de remplir 5 camions. Échec. Il efface tout son travail et recommence de zéro pour essayer 6 camions.
- Méthode de l'article : Le détective essaie 5 camions. Échec. Il se souvient de pourquoi ça a échoué (par exemple : "Il est impossible de mettre 3 gros canapés dans un seul camion"). Quand il teste 6 camions, il utilise immédiatement cette leçon pour ne pas perdre de temps à essayer l'impossible. Il réutilise ses erreurs passées pour aller plus vite.

🏆 Le Duel : Nos Détectives vs Les Géants de l'Industrie

Les chercheurs ont mis leur méthode à l'épreuve contre des logiciels industriels très puissants (comme OR-Tools, CPLEX et Gurobi), qui sont les "champions du monde" actuels de l'optimisation.

Les résultats sont surprenants :

La preuve absolue : Les logiciels industriels sont souvent très bons pour trouver une solution rapide (un bon arrangement), mais ils ont du mal à prouver que c'est le meilleur arrangement possible. Ils disent : "Voici un bon camion, c'est probablement le mieux".
La victoire du SAT : La méthode de l'article a prouvé mathématiquement qu'elle trouvait le meilleur arrangement possible pour 2 à 3 fois plus de cas que les logiciels industriels.
L'analogie : Imaginez que vous cherchez le chemin le plus court pour aller à l'école. Les logiciels industriels trouvent un chemin très rapide, mais ne sont pas sûrs qu'il n'y en a pas un plus court. Le détective SAT, lui, vous dit : "J'ai vérifié tous les chemins possibles, celui-ci est le seul et unique chemin le plus court."

💡 En résumé

Cette recherche montre que pour des problèmes complexes de découpe et de rangement, la logique pure (SAT) est souvent plus puissante que les méthodes de calcul traditionnelles, surtout quand on a beaucoup d'objets identiques à ranger.

C'est comme si, au lieu d'essayer de deviner la meilleure façon de remplir un camion, on avait inventé un détective qui, en écoutant les leçons de ses échecs précédents, arrive à prouver mathématiquement qu'il n'existe aucune autre façon de faire mieux.

Le mot de la fin : Pour les usines, cela signifie moins de gaspillage de matière (moins de chutes de verre ou de tissu) et des camions mieux remplis, ce qui économise de l'argent et de l'énergie.

1. Problématique : Le Problème de Découpe 2D (2D-CSSP)

L'article aborde le Problème de Découpe de Stock Unique en Deux Dimensions (2D-CSSP). Il s'agit d'un problème central en fabrication (acier, verre, textile, meubles) consistant à découper une liste d'items rectangulaires à partir de feuilles de stock identiques, tout en minimisant le nombre de feuilles utilisées.

Définition : Contrairement au problème classique de bin packing (2D-BPP) où chaque item est unique, le 2D-CSSP implique des types d'items avec des demandes multiples ( $d_t \ge 1$ ).
Complexité : Le problème est NP-difficile. La demande multiple crée une explosion combinatoire : un type d'item avec une demande de 20 génère 20 copies, multipliant les variables géométriques et les contraintes de non-chevauchement.
Défis actuels :
- Les méthodes exactes (génération de colonnes, MIP) peinent à scaler lorsque les demandes sont élevées.
- Les méthodes heuristiques sont rapides mais ne fournissent pas de certificats d'optimalité.
- Les solveurs commerciaux (CP, MIP) échouent souvent à prouver l'optimalité sur des instances de taille modérée dans des temps raisonnables.

2. Méthodologie : Un Cadre Basé sur SAT/MaxSAT

Les auteurs proposent le premier cadre basé sur la Satisfiabilité Booléenne (SAT) et le MaxSAT spécifiquement conçu pour le 2D-CSSP.

A. Encodage Propositionnel

L'approche repose sur une expansion des demandes : chaque type d'item $t$ est décomposé en $d_t$ copies distinctes. Pour chaque copie, des variables de décision sont définies :

Assignation de feuille : Variable indiquant sur quelle feuille la copie est placée.
Coordonnées : Encodées via une encodage d'ordre (order encoding) pour représenter les positions $(x, y)$ avec un nombre linéaire de variables booléennes.
Rotation : Variable binaire pour autoriser ou interdire une rotation à 90°.

Contraintes Clés :

Non-chevauchement conditionnel : C'est l'innovation majeure. Les contraintes de non-chevauchement ne sont activées que si deux copies sont assignées à la même feuille. Cela évite d'ajouter des contraintes géométriques inutiles entre items sur des feuilles différentes.
Élimination des orientations infeasibles : Une règle de symétrie fixe automatiquement la variable de rotation si une seule orientation permet de faire tenir l'item dans la feuille.

B. Stratégies de Résolution

Trois approches sont comparées pour minimiser le nombre de feuilles $k$ :

SAT Non-Incrémental avec Recherche Binaire : On construit le problème de zéro pour chaque valeur de $k$ testée (via recherche binaire entre une borne inférieure et supérieure).
SAT Incrémental : On construit une seule formule pour la borne supérieure. Pour tester une valeur $k$ , on utilise des hypothèses (assumptions) pour désactiver les feuilles excédentaires. Les clauses apprises (conflict clauses) lors des échecs précédents sont conservées et réutilisées, ce qui est crucial pour les instances à forte demande.
MaxSAT Partiel Pondéré : L'objectif (minimiser $k$ ) est encodé directement via des clauses souples, permettant de trouver l'optimum en une seule invocation de solveur, bien que cela puisse engendrer des surcoûts de calcul.

C. Brise-Symétrie

Pour contrer l'explosion de l'espace de recherche due à l'indiscernabilité des copies d'un même type, quatre règles de brise-symétrie sont appliquées :

Contraintes sur les grands items.
Ordre fixe pour les items de même taille (une copie ne peut pas être strictement à gauche d'une copie précédente du même type).
Élimination des orientations infeasibles (déjà mentionnée).
Ordre des feuilles (les feuilles sont utilisées séquentiellement pour éviter les permutations de feuilles).

3. Contributions Principales

Premier encodage SAT pour le 2D-CSSP : Une formulation qui gère nativement la dimension de la demande via des contraintes conditionnelles et des variables d'assignation.
Règle d'élimination des orientations : Une généralisation des règles existantes qui fixe la rotation dès qu'une orientation est physiquement impossible, réduisant l'espace de recherche.
Analyse comparative des stratégies SAT : Mise en évidence que le choix entre SAT incrémental et non-incrémental dépend de la structure du problème (notamment de la présence de rotation).
Benchmark à grande échelle : Une comparaison rigoureuse sur 30 instances (suite Cui-Zhao) contre des solveurs industriels de pointe (OR-Tools, CPLEX, Gurobi).

4. Résultats Expérimentaux

Les expériences ont été menées sur une suite de 30 instances avec des demandes allant jusqu'à 45 et des dimensions de feuilles variées.

Performance par rapport aux solveurs commerciaux :
- L'approche SAT propose 2 à 3 fois plus de certificats d'optimalité que les meilleurs solveurs commerciaux.
- Sans rotation : La configuration SAT incrémentale avec brise-symétrie (CSP INC SB) prouve l'optimalité de 16 instances (contre 7 pour le meilleur solveur commercial OR-Tools) avec un écart moyen de 9,71 % (contre 12,03 %).
- Avec rotation : La configuration SAT non-incrémentale (CSP R) prouve l'optimalité de 18 instances (contre 6 pour les solveurs commerciaux) avec un écart réduit à 3,24 % (contre 4,63 %).
Comparaison des stratégies SAT :
- Sans rotation : Le SAT incrémental est supérieur. Les clauses apprises sur les copies d'un même type sont transférables efficacement entre les itérations de recherche binaire.
- Avec rotation : Le SAT non-incrémental devient plus performant. La rotation double le nombre de variables et triple le nombre de clauses, rendant la base de clauses du SAT incrémental trop lourde et diluant les connaissances apprises.
Qualité des solutions : Les solveurs SAT atteignent des écarts d'optimalité nettement inférieurs à ceux des solveurs MIP et CP, même lorsque ces derniers trouvent des solutions faisables.

5. Signification et Conclusion

Cet article démontre que les méthodes basées sur la logique booléenne (SAT/MaxSAT) sont particulièrement adaptées aux problèmes de découpe avec demandes multiples, un domaine où les méthodes traditionnelles (MIP/CP) peinent souvent.

Avantage clé : La capacité des solveurs SAT modernes (basés sur CDCL) à apprendre et réutiliser des clauses de conflit géométriques, exploitant ainsi la structure de symétrie induite par les demandes multiples.
Impact : La méthode propose non seulement des solutions de haute qualité, mais surtout des certificats d'optimalité là où les solveurs industriels échouent.
Perspectives : Les auteurs suggèrent l'intégration de bornes inférieures plus serrées, des hybrides avec la génération de colonnes (où SAT résout le sous-problème de prix) et l'extension à des stocks de tailles hétérogènes.

En résumé, cette étude établit un nouvel état de l'art pour le 2D-CSSP, prouvant que l'approche SAT, correctement encodée et adaptée à la structure de la demande, surpasse les plateformes d'optimisation industrielle standard.