Accelerating Discrete Facility Layout Optimization: A Hybrid CDCL and CP-SAT Architecture

Resumo Técnico: Aprendizado de Cláusulas Impulsionado por Conflitos com Heurísticas VSIDS para Layout de Instalações Discretas

Definição do Problema
O artigo aborda o Problema de Layout de Instalações Discretas (FLP), focando especificamente em layouts baseados em grade onde máquinas devem ser atribuídas a slots sob restrições combinatórias densas. Essas restrições incluem atribuição um para um, requisitos de adjacência (devem ser vizinhos), restrições de separação (vizinhos proibidos), células bloqueadas (corredores) e alocação em múltiplos andares. Enquanto formulações canônicas frequentemente tratam o FLP como um Problema de Atribuição Quadrática (QAP), instâncias do mundo real introduzem restrições ricas em lógica que criam uma estrutura combinatória densa. O estudo investiga se solucionadores SAT modernos que utilizam Aprendizado de Cláusulas Impulsionado por Conflitos (CDCL) com a heurística de Soma Decrescente Independente do Estado da Variável (VSIDS) podem explorar efetivamente essa estrutura e, sob quais condições, eles se comparam favoravelmente às abordagens estabelecidas de Programação por Restrições (CP-SAT) e Programação Linear Inteira Mista (MILP).

Metodologia
Os autores desenvolveram uma ferramenta de benchmarking unificada em Python para realizar comparações controladas entre três paradigmas de solucionadores:

1. CDCL+VSIDS: Implementado usando PySAT com back-ends Glucose4 e MiniSat22. A viabilidade do layout é codificada em Forma Normal Conjuntiva (CNF) usando variáveis booleanas ($z_{ij}$) para atribuições máquina-slot. As restrições são codificadas via restrições de cardinalidade (usando contadores sequenciais ou totalizadores para reduzir a contagem de cláusulas), cláusulas de adjacência/separação e cláusulas unitárias para células bloqueadas. A otimização é tratada considerando o CDCL como um motor de viabilidade, enquanto objetivos de otimização são abordados por meio de arquiteturas híbridas.
2. CP-SAT: Implementado via Google OR-Tools, aproveitando restrições globais e raciocínio pseudo-booleano.
3. MILP: Implementado via PuLP com CBC, utilizando formulações QAP linearizadas.

Desenho Experimental
O estudo utilizou dados sintéticos para isolar o desempenho algorítmico da variância do mundo real. Os experimentos variaram em:

• Tamanhos de Grade: Variando de 2×2 a 6×6 (com 5×5 servindo como limite para falha do MILP e 6×6 como teste limite para intratabilidade).
• Densidade de Restrições ($\rho$): Variando de 0,05 a 0,35.
• Tipos Estruturais: Apenas atribuição, com restrição de adjacência, com restrição de separação e mistos.
• Simetria: Testes foram executados com e sem fixação posicional da primeira máquina para quebrar a simetria.
• Tempo Limite: 10 segundos para verificações de viabilidade e 60 segundos para ensaios de otimização.

Principais Descobertas

• Detecção de Viabilidade: O CDCL+VSIDS demonstra desempenho de tempo de execução quase constante em tamanhos de grade e densidades de restrições variáveis, superando o CP-SAT em uma a duas ordens de magnitude e o MILP por margens ainda maiores. O CDCL se destaca na poda do espaço de busca para viabilidade pura.
• Otimização: Embora o CDCL seja rápido em encontrar uma solução, ele não pode otimizar nativamente objetivos suaves (como minimizar a distância de Manhattan) sem MaxSAT ou afunilamento iterativo de limites, o que adiciona sobrecarga. O CP-SAT se destaca na otimização híbrida lógico-numérica, provando ótimos globais para instâncias 5×5 e 6×6 onde o MILP falhou em convergir dentro do limite de tempo.
• Limitações do MILP: O MILP exibe desaceleração exponencial à medida que o tamanho da grade e a densidade de restrições aumentam, lutando com os relaxamentos lineares fracos causados por disjunções big-M e termos pareados densos.
• Quebra de Simetria: Fixar a posição de uma máquina melhorou significativamente os tempos de execução do CP-SAT (27%) e do MILP (50%), mas causou uma leve desaceleração para o CDCL, pois as cláusulas adicionadas aumentaram a complexidade da fórmula sem fornecer os mesmos benefícios de poda em um contexto de aprendizado de cláusulas.

Arquiteturas Híbridas
Para aproveitar a velocidade do CDCL e a qualidade de otimização do CP-SAT, os autores propuseram duas arquiteturas híbridas:

1. Enumeração Profunda (Arquitetura A): O CDCL enumera um grande conjunto de layouts viáveis (75.000 amostras), e o CP-SAT seleciona o melhor. Essa abordagem encontrou uma solução viável (Obj=22,0) em ~24 segundos, significativamente mais rápido que a linha de base do CP-SAT de 60 segundos, embora não tenha atingido o ótimo global (Obj=13,0).
2. Inicialização Quente (Arquitetura B): O CDCL gera um único indicativo viável rápido (um limite superior) e o injeta no processo de ramificação e limitação do CP-SAT. Essa abordagem atingiu o ótimo global (Obj=13,0) com uma vantagem de tempo de execução validada sobre a linha de base de inicialização fria, demonstrando que indicativos impulsionados pelo CDCL podam efetivamente os ramos iniciais da árvore de busca.

Significado e Alegações
O artigo afirma que o caminho mais eficaz para a otimização de layout de instalações discretas não é substituir solucionadores exatos, mas acelerá-los usando indicativos de viabilidade impulsionados pelo CDCL. O estudo estabelece que:

• O CDCL+VSIDS possui "dominância inigualável" na detecção de viabilidade pura para FLPS baseados em grade e ricos em lógica, resolvendo regras complexas de adjacência e separação ordens de magnitude mais rápido que CP-SAT ou MILP.
• O CDCL puro luta com otimização consciente de custos, tornando-o inadequado como otimizador autônomo para esses problemas.
• Arquiteturas híbridas, especificamente a abordagem de Inicialização Quente, conectam com sucesso a lacuna entre satisfatibilidade rápida e otimalidade comprovada. Ao usar o CDCL para fornecer um limite superior válido, o sistema híbrido alcança ótimos globais com vantagens algorítmicas de velocidade validadas sobre linhas de base de inicialização fria.

Os autores concluem que, embora o CDCL raramente seja aplicado a FLPS de fábrica em escala total devido a incompatibilidades de otimização e sobrecargas de codificação, sua integração como motor de viabilidade dentro de um framework híbrido oferece uma solução robusta para problemas de layout de alta complexidade.