💻 computer science

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

Este artículo presenta un marco basado en SAT y MaxSAT para resolver el problema de corte de stock bidimensional con un solo tamaño, el cual supera a herramientas comerciales como CPLEX y Gurobi al certificar más instancias como óptimas y reducir la brecha de optimalidad mediante estrategias de asignación de hojas y eliminación de orientaciones inviables.

Autores originales: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Publicado 2026-04-03

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

¡Claro que sí! Imagina que eres el jefe de una fábrica de muebles, una empresa de vidrio o una tienda de telas. Tu trabajo diario es un rompecabezas gigante: tienes grandes láminas de material (como una hoja de papel de 4x4 metros) y necesitas cortar cientos de piezas más pequeñas (mesas, ventanas, camisas) para cumplir con los pedidos de tus clientes.

El objetivo es simple: usar la menor cantidad de láminas posibles para que no te sobre material desperdiciado. Pero hay un truco: si tienes 20 pedidos de la misma mesa, no puedes tratarlos como una sola pieza; tienes que cortar 20 veces. Esto convierte el problema en una locura matemática.

Aquí es donde entra este artículo. Los autores (Tuyen, Chi y Khanh) han creado un nuevo "cerebro" digital para resolver este rompecabezas mejor que las máquinas más caras del mundo.

1. El Problema: El Caos de las Copias

Imagina que tienes que cortar 50 piezas idénticas.

El enfoque antiguo: Los programas tradicionales trataban cada una de las 50 piezas como un individuo único y diferente. Era como intentar organizar a 50 personas en una habitación, preguntando a cada una: "¿Te sientas aquí o allá?". Se volvía un caos inmenso y lento.
La idea de los autores: "¡Esperen! Todas esas 50 piezas son gemelas. Si una no cabe en un rincón, las 50 no caben". En lugar de tratarlas como 50 individuos, su nuevo sistema las agrupa y les dice: "Ustedes son un equipo, decidan juntos dónde van".

2. La Solución: El "Detective Lógico" (SAT)

Los autores usan una tecnología llamada SAT (Satisfacibilidad Booleana). Para entenderlo, imagina que SAT es un detective lógico extremadamente rápido que solo responde "Sí" o "No" a preguntas muy específicas.

La pregunta: "¿Es posible colocar todas las piezas en 3 láminas?"
La respuesta del detective: "¡No! Es imposible, porque dos piezas grandes chocarían".
La magia: Cuando el detective dice "No", no solo se rinde. Aprende una lección: "Ah, nunca más pondré dos piezas grandes juntas en la misma lámina". Guarda esa regla en su memoria.

3. Los Tres Estrategas

El equipo probó tres formas de usar a este detective para encontrar el número perfecto de láminas:

El Adivino (SAT No Incremental): El detective prueba con 3 láminas. Si falla, olvida todo y empieza de cero probando con 4. Es como si cada vez que fallas un examen, borras tu cerebro y empiezas a estudiar desde cero. Funciona bien si el examen es corto, pero lento si es largo.
El Estudiante Inteligente (SAT Incremental): Esta es la estrella cuando no hay rotación de piezas. El detective prueba con 3 láminas, falla, guarda sus lecciones, y luego prueba con 4 láminas sin olvidar nada. Usa lo que aprendió antes para ir más rápido. Es como estudiar para un examen final: si ya sabes que la fórmula A no funciona, no la vuelves a probar.
El Optimizador (MaxSAT): Este intenta ver todas las posibilidades a la vez para encontrar la solución perfecta de un solo golpe. Es muy potente, pero a veces se abruma con tanta información y se vuelve lento.

4. El Truco de la Rotación (Girar las piezas)

A veces, puedes girar una pieza 90 grados (como poner un libro de pie en lugar de acostado).

Sin girar: El "Estudiante Inteligente" (Incremental) gana por goleada porque las reglas que aprende se aplican perfectamente a todas las copias.
Con girar: El problema se vuelve mucho más complejo (como si las piezas pudieran cambiar de forma). Aquí, el "Adivino" (No Incremental) a veces funciona mejor porque reiniciar el cerebro le ayuda a no confundirse con tantas reglas nuevas.

5. ¿Cómo les fue contra los Gigantes?

Los autores pusieron a su sistema a competir contra los "jefes" de la industria: OR-Tools, CPLEX y Gurobi (que son como los Ferrari de la optimización, muy caros y potentes).

El resultado: ¡El sistema de los autores ganó!
- Mientras los Ferrari lograban demostrar que una solución era la mejor posible en solo 6 o 7 casos, el sistema de los autores lo logró en 16 a 18 casos.
- Además, cuando no podían probar que era la mejor, el sistema de los autores se acercaba mucho más a la perfección (menos desperdicio de material) que los otros.

En Resumen

Imagina que tienes que empaquetar una mudanza.

Los métodos antiguos son como intentar meter todo en cajas probando una por una, olvidando lo que ya intentaste.
Los métodos comerciales son como tener una caja de herramientas muy cara que a veces se atasca.
Este nuevo método es como tener un organizador genio que, en lugar de probar a ciegas, aprende de cada error, agrupa las cosas idénticas y te dice exactamente cuántas cajas necesitas para que no sobre ni un centímetro de espacio.

Es una prueba de que, a veces, no necesitas un motor más grande (más potencia bruta), sino un cerebro más inteligente (mejor lógica) para resolver los problemas más difíciles de la fabricación.

Resumen Técnico: Resolución del Problema de Corte de Stock Bidimensional con SAT y MaxSAT

1. Definición del Problema

El artículo aborda el Problema de Corte de Stock Bidimensional de Tamaño Único (2D-CSSP). Este es un problema de optimización combinatoria fundamental en la manufactura (corte de acero, vidrio, textiles, etc.), donde el objetivo es cortar una lista de artículos rectangulares de diferentes tipos desde hojas de material idénticas, satisfaciendo la demanda de cada tipo ( $d_t \ge 1$ ) y minimizando el número total de hojas utilizadas.

Desafío Principal: A diferencia del Problema de Empaquetamiento Bidimensional (2D-BPP) donde cada artículo es único, el 2D-CSSP implica múltiples copias de cada tipo de artículo. Esto genera una explosión combinatoria significativa en el espacio de búsqueda debido a la multiplicación de variables geométricas y a la simetría inducida por las demandas (las copias de un mismo tipo son intercambiables).
Complejidad: El problema es NP-duro. Los métodos exactos tradicionales (como la generación de columnas o modelos MIP) sufren de escalabilidad pobre cuando las demandas son altas, mientras que los métodos heurísticos no pueden certificar la optimalidad de la solución.

2. Metodología y Enfoque Propuesto

Los autores proponen un marco de trabajo basado en Satisfacibilidad Booleana (SAT) y MaxSAT, que es la primera formulación de este tipo para el 2D-CSSP.

A. Codificación SAT:

Expansión por Demanda: En lugar de tratar los tipos de artículos abstractamente, el método expande la demanda, creando copias individuales ( $c_{t,1}, \dots, c_{t,d_t}$ ) para cada tipo.
Variables de Decisión:
- Asignación de hoja ( $\sigma_c$ ): A qué hoja se asigna cada copia.
- Coordenadas ( $x_c, y_c$ ): Posición de la esquina inferior izquierda, codificadas mediante ordenamiento (order encoding) para mantener la compacidad.
- Rotación ( $r_c$ ): Indicador binario si el artículo está rotado 90°.
Restricciones No Superpuestas Condicionales: Este es el núcleo de la innovación. Las restricciones de no superposición se activan solo si dos copias están asignadas a la misma hoja. Esto se logra mediante cláusulas condicionales que incluyen las variables de asignación de hoja, evitando la explosión de restricciones entre artículos en hojas diferentes.
Eliminación de Simetría: Se implementan cuatro reglas para reducir el espacio de búsqueda:
1. Restricciones de artículos grandes (si no caben juntos, se fija su posición relativa).
2. Ordenamiento de artículos del mismo tamaño (evita permutaciones de copias idénticas).
3. Eliminación de orientación inviable: Si un artículo solo cabe en una orientación dentro de la hoja, la variable de rotación se fija automáticamente.
4. Ordenamiento de hojas: Se fuerza el uso de hojas en orden de índice para evitar reetiquetados redundantes.

B. Estrategias de Resolución:
Se comparan tres enfoques para minimizar el número de hojas ( $k$ ):

SAT No Incremental con Búsqueda Binaria: Genera un nuevo modelo SAT para cada valor de $k$ probado.
SAT Incremental con Búsqueda Binaria: Construye un modelo para el límite superior de hojas y utiliza "asunciones" para desactivar hojas sobrantes. Las cláusulas aprendidas (conflictos) en iteraciones previas se reutilizan, lo cual es crucial para problemas con alta demanda.
MaxSAT Parcial Ponderado: Codifica el objetivo de minimización directamente en el solver, tratando el uso de hojas como cláusulas "blandas" (soft clauses) a minimizar.

3. Contribuciones Clave

Primera Codificación SAT para 2D-CSSP: Introduce una capa de codificación que maneja la replicación por demanda y la activación condicional de restricciones geométricas.
Regla de Eliminación de Orientación Inviable: Una generalización de reglas anteriores que fija la rotación de artículos cuando solo una orientación es geométricamente posible, mejorando la eficiencia sin perder completitud.
Análisis de la Interacción Demanda-Rotación: Demuestra que la efectividad relativa de los enfoques SAT (incremental vs. no incremental) depende de si la rotación está habilitada.
Comparación a Gran Escala: Evaluación exhaustiva contra solvers comerciales (OR-Tools, CPLEX, Gurobi) en un conjunto de 30 instancias estándar (Cui-Zhao).

4. Resultados Experimentales

Los experimentos se realizaron en un conjunto de 30 instancias con demandas de 1 a 45 y dimensiones de hoja variables, con un límite de tiempo de 1800 segundos.

Rendimiento General: Los enfoques basados en SAT superaron significativamente a los solvers comerciales en términos de certificación de optimalidad.
- Sin Rotación: La configuración SAT Incremental con Simetría (CSP INC SB) certificó 16 instancias como óptimas, más del doble que el mejor solver comercial (7 instancias). El gap de optimalidad fue del 9.71% frente al 12.03% del mejor comercial.
- Con Rotación: La configuración SAT No Incremental (CSP R) certificó 18 instancias óptimas, tres veces más que el mejor comercial (6 instancias). El gap se redujo drásticamente al 3.24% (vs 4.63% comercial).
Comparativa de Enfoques SAT:
- Sin rotación: El SAT Incremental es superior porque las cláusulas de conflicto aprendidas sobre la geometría de las copias de un mismo tipo son válidas y reutilizables entre iteraciones de búsqueda.
- Con rotación: El SAT No Incremental se vuelve más efectivo. La rotación aumenta el tamaño de la fórmula (más variables y cláusulas), lo que hace que la base de datos de cláusulas en el enfoque incremental sea demasiado grande y contenga información irrelevante que diluye el aprendizaje.
Comparativa con Solvers Comerciales:
- OR-Tools (CP-SAT): Fue el competidor comercial más fuerte, encontrando muchas soluciones factibles cercanas al óptimo, pero falló consistentemente en probar la optimalidad de esas soluciones.
- CPLEX y Gurobi (MIP): Tuvieron dificultades para certificar optimalidad en instancias medianas, con gaps significativamente más altos (superiores al 13-21%).
- Conclusión: El mecanismo de prueba de CDCL (Conflict-Driven Clause Learning) en SAT proporciona certificados de optimalidad mucho más fuertes que los enfoques basados en programación lineal entera o programación por restricciones estándar para este tipo de problemas.

5. Significado e Impacto

Este trabajo demuestra que los métodos basados en lógica proposicional (SAT) son una alternativa viable y superior a los métodos tradicionales de programación matemática para problemas de corte de stock con alta demanda.

Ventaja Clave: La capacidad de reutilizar conocimiento geométrico (cláusulas de conflicto) a través de las copias de artículos idénticos permite escalar mejor que los métodos MIP cuando las demandas son altas.
Aplicabilidad: Ofrece a la industria una herramienta capaz no solo de encontrar buenas soluciones, sino de garantizar matemáticamente que no existe una solución mejor, algo que los solvers comerciales actuales no logran en la mayoría de los casos prácticos de este problema.
Futuro: Los autores sugieren explorar límites inferiores más ajustados, híbridos con generación de columnas (donde SAT resuelve el subproblema de precios) y la extensión a tamaños de stock heterogéneos.

En resumen, el artículo establece un nuevo estado del arte para el 2D-CSSP, demostrando que la codificación inteligente de restricciones condicionales y el uso estratégico de SAT incremental/no incremental pueden superar a las plataformas de optimización industrial más avanzadas en términos de certidumbre de optimalidad.