Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

Resumo Técnico: Transferência de Aprendizado de Embeddings de Otimização Fundacional para Representações SAT Não Supervisionadas

1. Problema e Motivação

O artigo aborda o desafio de criar representações estruturais robustas e generalizáveis para problemas de satisfação booleana (SAT). Atualmente, os modelos baseados em Redes Neurais em Grafos (GNNs) para SAT dependem fortemente de:

• Rótulos gerados por solvers: O treinamento supervisionado exige dados rotulados por solucionadores de SAT, o que é custoso e limita a generalização.
• Especialização de domínio: Modelos treinados para uma tarefa ou distribuição específica frequentemente falham ao generalizar para outros domínios ou escalas de instâncias.

Por outro lado, embeddings de otimização fundacional (como o modelo Forge para Programação Inteira Mista - MIP) demonstraram sucesso em aprender representações genéricas através de pré-treinamento não supervisionado em grandes corpora heterogêneos. A questão central deste trabalho é: as representações aprendidas para problemas de otimização (MIP) podem generalizar e ser transferidas para problemas de decisão (SAT)?

2. Metodologia

Os autores propõem uma abordagem de transferência de aprendizado adaptando a arquitetura do Forge (originalmente para MIP) para instâncias SAT. O processo baseia-se na equivalência estrutural entre os dois problemas:

• Codificação SAT-to-MIP: Fórmulas em Forma Normal Conjuntiva (CNF) são convertidas em instâncias de MIP 0-1. Isso permite representar o problema SAT como um grafo bipartido (nós de restrições/cláusulas e nós de variáveis), idêntico à representação usada para MIPs.
• Arquitetura Base (Forge): O modelo utiliza um codificador GNN (GraphSAGE de duas camadas) que gera embeddings latentes, discretizados via um dicionário de vetores quantizados (Vector Quantization - VQ). Um decodificador reconstrói as características dos nós e as arestas, permitindo o pré-treinamento não supervisionado sem rótulos de solver.

O estudo compara três variantes de transferência:

1. Forge-MIP (Transferência Zero-Mudança): Reutiliza diretamente o modelo pré-treinado em MIP e suas características específicas de MIP, aplicando-o a instâncias SAT codificadas como MIP.
2. Forge-MIP-SAT (Transferência Adaptada de Características): Mantém os pesos pré-treinados do MIP, mas substitui as características dos nós (features) por características específicas de SAT (ex: largura da cláusula, contagem de literais positivos/negativos, graus das variáveis).
3. Forge-SAT (Modelo Nativo SAT): Mantém a arquitetura do Forge, mas descarta os pesos pré-treinados de MIP. O modelo é pré-treinado do zero em instâncias SAT usando características específicas de SAT.

3. Contribuições Principais

1. Adaptação Arquitetural: Demonstração de que a arquitetura fundacional do Forge pode ser adaptada para SAT através de uma pipeline de codificação SAT-to-MIP e características de nós específicas.
2. Transferência de Pesos: Evidência empírica de que embeddings pré-treinados em MIP (Forge-MIP) já capturam estruturas úteis em SAT, e que a especialização de características (Forge-MIP-SAT) melhora o desempenho.
3. Modelo Fundacional Nativo: Introdução do Forge-SAT, um modelo pré-treinado especificamente para SAT que reutiliza o paradigma de treinamento do Forge, permitindo a geração de embeddings significativos "out-of-the-box".
4. Avaliação Não Supervisionada: Primeira avaliação que demonstra a capacidade de embeddings fundacionais de otimização transferirem-se para domínios de satisfação de restrições, focando em tarefas não supervisionadas como agrupamento (clustering) e identificação de distribuição.
5. Código Aberto: Disponibilização de todos os modelos pré-treinados e pipelines de treinamento.

4. Resultados Experimentais

Os experimentos foram conduzidos no conjunto de dados G4SATBench, utilizando instâncias "Hard" de 7 tipos de problemas diferentes (divididos em satisfiáveis e insatisfiáveis). A métrica principal foi a qualidade do agrupamento (clustering) das instâncias.

• Métricas: Normalized Mutual Information (NMI) e Purity.
• Desempenho:
  • Baseline Estático (Static-SAT): Alcançou um NMI de 0.74, servindo como uma base forte.
  • Forge-MIP: Melhorou para 0.76, provando que o conhecimento de MIP transfere-se para SAT.
  • Forge-MIP-SAT: Alcançou 0.77, mostrando que a combinação de pesos de MIP com características de SAT é eficaz.
  • Forge-SAT: Alcançou o melhor desempenho com NMI de 0.79 e Purity de 0.66.
• Visualização: O modelo Forge-SAT conseguiu formar 13 dos 14 clusters ideais (tipos de problema + satisfatibilidade), separando claramente as instâncias satisfiáveis das insatisfiáveis dentro do mesmo tipo de problema. Os modelos baseados em MIP (Forge-MIP e Forge-MIP-SAT) produziram clusters menos compactos, mas ainda superiores à linha de base estática.

5. Significado e Conclusão

Este trabalho representa um avanço significativo ao estabelecer a viabilidade de modelos fundacionais unificados para problemas de otimização (MIP) e decisão (SAT).

• Generalização Cross-Domain: Demonstra que estruturas matemáticas subjacentes são compartilhadas entre MIP e SAT, permitindo que representações aprendidas em um domínio beneficiem o outro.
• Redução de Dependência de Solvers: A abordagem não supervisionada elimina a necessidade de rótulos gerados por solvers de SAT para criar representações ricas, facilitando a aplicação em novos domínios onde solvers podem ser lentos ou indisponíveis.
• Futuro: Os autores sugerem que essa linha de pesquisa pode ser estendida para Problemas de Satisfação de Restrições (CSP) e Programação por Restrições (CP), visando um único modelo fundacional capaz de cobrir todo o espectro de problemas combinatórios.

Em suma, o artigo prova que é possível "reutilizar" o conhecimento estrutural de modelos de otimização massivos para resolver problemas de lógica booleana, abrindo caminho para uma nova geração de ferramentas de IA unificadas para raciocínio combinatório.