💻 computer science

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

Este artigo apresenta um framework baseado em SAT e MaxSAT para resolver o Problema de Corte de Estoque Bidimensional de Tamanho Único, que supera métodos comerciais como OR-Tools, CPLEX e Gurobi ao certificar mais instâncias como ótimas e reduzir as lacunas de otimalidade em benchmarks padrão.

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

Publicado 2026-04-03

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é o gerente de uma grande fábrica de móveis ou de vidro. Todos os dias, você recebe uma pilha de pedidos: "Precisamos de 30 mesas retangulares, 20 cadeiras e 50 prateleiras". O problema é que você só tem grandes chapas de madeira ou vidro (os "estoques") e precisa cortar todas essas peças a partir delas, desperdiçando o mínimo possível de material.

Se você cortar errado, sobra muita sobra (lixo) e você perde dinheiro. Se usar muitas chapas, o custo sobe. O objetivo é: cortar tudo usando o menor número possível de chapas.

Esse é o problema que os autores deste artigo resolveram. Eles criaram uma nova maneira de usar computadores para encontrar a solução perfeita, e a explicação abaixo usa analogias simples para mostrar como eles fizeram isso.

1. O Problema: O "Quebra-Cabeça" Infinito

O problema é chamado de "Corte de Estoque Bidimensional". Pense nele como um quebra-cabeça gigante, mas com uma complicação: você não tem apenas uma peça de cada tipo. Você tem várias cópias de cada peça (ex: 30 mesas iguais).

Isso torna o problema explosivo. Se você tentar colocar 30 mesas iguais em uma prateleira, o computador precisa verificar milhões de combinações. Métodos antigos de computador (como os usados por grandes empresas de software) conseguiam encontrar uma solução "boa", mas muitas vezes não conseguiam provar que era a melhor solução possível em um tempo razoável. Eles ficavam "travados" tentando provar que não existia um jeito melhor.

2. A Solução: O Detetive Lógico (SAT)

Os autores decidiram usar uma técnica chamada SAT (Satisfatibilidade Booleana). Para entender, imagine que o computador não é um matemático calculando áreas, mas sim um detetive lógico extremamente rápido.

A Abordagem Antiga: Tentar encaixar as peças uma por uma, como se estivesse jogando Tetris manualmente.
A Abordagem Nova (SAT): O detetive transforma o problema em uma série de perguntas de "Sim" ou "Não".
- "A mesa 1 está na chapa A?" (Sim/Não)
- "A mesa 1 está à esquerda da cadeira 2?" (Sim/Não)
- "A mesa 1 está girada 90 graus?" (Sim/Não)

O computador tenta responder a todas essas perguntas ao mesmo tempo. Se ele encontrar uma combinação de "Sim" e "Não" que não quebre nenhuma regra (como peças se sobrepondo), ele encontrou uma solução válida.

3. O Truque de Mestre: "Se estiver na mesma chapa..."

O grande segredo do artigo é como eles lidam com as cópias idênticas.
Imagine que você tem 30 mesas iguais. Em vez de criar 30 regras separadas para cada mesa, o computador usa uma regra inteligente:

"Só precisamos garantir que a Mesa 1 e a Mesa 2 não se toquem SE elas estiverem na mesma chapa."

Se a Mesa 1 está na Chapa A e a Mesa 2 está na Chapa B, o computador ignora a regra de "não se tocarem", porque elas estão em lugares diferentes. Isso economiza uma quantidade enorme de trabalho mental para o computador.

4. As Três Estratégias de Detetive

Os autores testaram três formas de usar esse detetive:

O Adivinho (Busca Binária Não-Incremental): O computador chuta um número de chapas (ex: "Será que 10 chapas bastam?"). Se não der, ele tenta 11, depois 9, e assim por diante, estreitando a busca. É como tentar adivinhar um número entre 1 e 100.
O Acumulador de Experiência (SAT Incremental): Aqui está a mágica. Se o computador tenta com 10 chapas e descobre que é impossível, ele aprende por que é impossível (ex: "Ah, 3 mesas largas nunca cabem juntas"). Quando ele tenta com 11 chapas, ele não joga fora esse aprendizado. Ele usa a lição anterior para pular etapas e resolver mais rápido. É como um aluno que, ao errar uma questão de matemática, aprende o erro e não o comete mais na próxima prova.
O Otimizador de Peso (MaxSAT): Em vez de chutar números, ele tenta minimizar o desperdício de uma vez só, pesando as opções. Funciona bem, mas às vezes é mais lento.

5. O Resultado: Vencendo os Gigantes

Os autores testaram seu método contra os softwares mais famosos do mundo (como OR-Tools, CPLEX e Gurobi), que são usados por grandes indústrias.

O Resultado: O novo método deles conseguiu provar que encontrou a solução perfeita (o número mínimo absoluto de chapas) em duas a três vezes mais casos do que os softwares comerciais.
A Analogia: Imagine uma corrida de Fórmula 1. Os softwares comerciais são carros muito rápidos que chegam perto da linha de chegada, mas muitas vezes não conseguem provar que foram os primeiros. O método dos autores é como um carro que, além de ser rápido, tem um sistema que prova matematicamente que ninguém pode passar por ele.

6. Quando Girar as Peças?

Um detalhe curioso: às vezes, virar a peça (girar 90 graus) ajuda a encaixar melhor.

Sem giro: O método "Acumulador de Experiência" (Incremental) foi o campeão, porque as lições aprendidas serviam perfeitamente para as próximas tentativas.
Com giro: O problema ficou tão complexo que as lições antigas às vezes atrapalhavam. Nesse caso, o método "Adivinho" (que reinicia a cada tentativa) funcionou melhor.

Resumo Final

Este artigo apresenta uma nova maneira de usar a lógica pura para resolver problemas de corte industrial. Em vez de tentar "adivinhar" onde colocar as peças, eles transformaram o problema em um jogo de lógica onde o computador elimina impossibilidades de forma brilhante.

A lição para o dia a dia: Às vezes, a melhor maneira de resolver um problema gigante não é tentar fazer tudo de uma vez, mas sim dividir em perguntas simples de "Sim/Não", aprender com os erros anteriores e usar essa sabedoria para não repetir os mesmos tropeços. O resultado é menos desperdício de material e mais economia para as fábricas.

Resumo Técnico: Resolução do Problema de Corte de Estoque Bidimensional (2D-CSSP) com SAT e MaxSAT

1. O Problema (2D-CSSP)

O artigo aborda o Problema de Corte de Estoque Bidimensional de Tamanho Único (2D-CSSP). O objetivo é cortar uma lista de itens retangulares de tipos específicos a partir de folhas de estoque idênticas (com dimensões $W \times H$ ), atendendo à demanda de cada tipo ( $d_t$ ) e minimizando o número total de folhas utilizadas.

Desafio Principal: Diferente do Problema de Empacotamento em Binários Bidimensional (2D-BPP), onde cada item é único, o 2D-CSSP envolve múltiplas cópias de cada tipo de item. Isso cria uma explosão combinatória significativa, pois a demanda multiplica tanto a dificuldade do subproblema de precificação quanto o número de variáveis geométricas.
Complexidade: O problema é NP-difícil. Métodos exatos tradicionais (como geração de colunas ou programação inteira mista - MIP) sofrem com a escalabilidade quando as demandas são altas, enquanto heurísticas não fornecem certificados de otimalidade.

2. Metodologia e Abordagem

Os autores propõem um framework baseado em SAT (Satisfatibilidade Booleana) e MaxSAT para resolver o problema de forma exata. A abordagem centraliza-se na expansão das demandas e no uso de restrições condicionais.

A. Codificação SAT Proposta:

Expansão de Demanda: Cada tipo de item $t$ com demanda $d_t$ é expandido em $d_t$ cópias individuais ( $c_{t,1}, \dots, c_{t,d_t}$ ).
Variáveis de Decisão:
- Atribuição de folha ( $\sigma_c$ ): Qual folha cada cópia ocupa.
- Posição ( $x_c, y_c$ ): Coordenadas do canto inferior esquerdo (codificadas via order encoding para manter a compactação).
- Rotação ( $r_c$ ): Indicador de rotação de 90°.
Restrições de Não-Overlap Condicionais: Esta é a inovação chave. As restrições de não sobreposição são ativadas apenas se duas cópias forem atribuídas à mesma folha. Isso evita a explosão de cláusulas que ocorreria se todas as cópias fossem forçadas a não se sobrepor globalmente, independentemente da folha.
- Cláusula típica: $\neg s_{c,j} \lor \neg s_{c',j} \lor \text{não-sobreposição}(c, c')$ .
Quebra de Simetria:
- SB1 & SB2: Restrições para itens grandes e ordenação de itens do mesmo tipo para evitar permutações redundantes.
- SB3 (Eliminação de Orientação Inviável): Se apenas uma orientação de um item couber na folha, a variável de rotação é fixada (eliminando a necessidade de busca).
- SB4: Ordenação das folhas para eliminar simetrias de reetiquetagem.

B. Estratégias de Resolução:
Os autores compararam três abordagens para minimizar o número de folhas ( $k$ ):

SAT Não-Incremental com Busca Binária: Gera uma nova fórmula $\Phi_m$ para cada tentativa de $k$ folhas. Descarta o estado do solver a cada iteração.
SAT Incremental com Busca Binária: Constrói uma fórmula para o limite superior ($UB$) e usa assumptions (suposições) para desativar folhas extras. Cláusulas de conflito aprendidas em tentativas falhas (ex: $k-1$ folhas) são reutilizadas para tentativas subsequentes, aproveitando a estrutura de demanda.
MaxSAT Parcial Ponderado: Codifica o objetivo diretamente, tratando o uso de folhas como cláusulas "soft" (suaves) a serem minimizadas, enquanto as restrições de viabilidade são "hard" (rígidas).

3. Contribuições Principais

Primeira Codificação SAT para 2D-CSSP: Introduz uma camada de codificação que lida com a replicação de itens por demanda e restrições de sobreposição condicionais, algo não abordado em trabalhos anteriores de empacotamento.
Regra de Eliminação de Orientação Inviável: Generaliza técnicas anteriores para fixar variáveis de rotação quando apenas uma orientação é geometricamente possível, reduzindo o espaço de busca.
Estudo Empírico de Estratégias: Demonstra que a eficácia relativa das abordagens (Incremental vs. Não-Incremental) depende criticamente da presença de rotação e da estrutura de demanda, invertendo tendências observadas no 2D-BPP.
Comparação em Larga Escala: Avaliação rigorosa contra solvers comerciais de ponta (OR-Tools, CPLEX, Gurobi) em um conjunto de benchmarks padrão (Cui-Zhao).

4. Resultados Experimentais

Os testes foram realizados em 30 instâncias do conjunto de benchmarks de Cui-Zhao, com limites de tempo de 1.800 segundos.

Desempenho Geral: A abordagem baseada em SAT superou significativamente os solvers comerciais em termos de número de instâncias provadas como ótimas e lacuna de otimalidade (gap).
- Sem Rotação: A configuração Incremental SAT com Quebra de Simetria (CSP INC SB) provou a otimalidade de 16 instâncias (o dobro dos melhores solvers comerciais, que provaram 7), com um gap médio de 9,71% (vs. 12,03% do melhor comercial).
- Com Rotação: A configuração SAT Não-Incremental (CSP R) provou a otimalidade de 18 instâncias (três vezes mais que os 6 do melhor comercial), com um gap de 3,24% (vs. 4,63% do OR-Tools).
Análise das Estratégias:
- Sem Rotação: O SAT Incremental foi superior. As cláusulas de conflito aprendidas sobre a impossibilidade geométrica de certos arranjos foram reutilizadas eficazmente entre as cópias de demanda.
- Com Rotação: O SAT Não-Incremental tornou-se mais eficaz. A rotação aumenta drasticamente o número de cláusulas (tripla expansão), diluindo o benefício da reutilização de cláusulas no método incremental. Começar "do zero" em cada passo da busca binária evitou o acúmulo de cláusulas irrelevantes.
Comparação com Comerciais:
- Solvers como OR-Tools (CP-SAT) frequentemente encontraram soluções viáveis próximas ao ótimo, mas falharam em provar a otimalidade dentro do limite de tempo.
- Solvers MIP (CPLEX, Gurobi) tiveram gaps altos (>13-21%) e provaram muito poucas instâncias.
- O mecanismo de prova do SAT (CDCL) mostrou-se superior para garantir a otimalidade em problemas de corte com demandas altas.

5. Significância e Conclusão

O trabalho demonstra que a lógica booleana (SAT) é uma ferramenta poderosa e subutilizada para problemas de corte e empacotamento com demandas múltiplas. A chave do sucesso foi a adaptação da codificação para lidar com a estrutura de demanda (cópias idênticas) através de restrições condicionais e a escolha inteligente da estratégia de resolução baseada no tamanho da fórmula (com ou sem rotação).

Os resultados sugerem que, para problemas industriais de corte onde a garantia de otimalidade é crucial, abordagens baseadas em SAT podem superar plataformas de otimização comercial estabelecidas, especialmente quando combinadas com técnicas de quebra de simetria específicas para o domínio. O código-fonte e os dados foram disponibilizados publicamente para reprodução e avanço futuro.