Resumo Técnico: Computação de Implicantes SAT Curtos via Codificações Ising/QUBO

1. Declaração do Problema

Muitas tarefas de raciocínio, incluindo explicação, diagnóstico e compressão de modelos, requerem atribuições parciais satisfatórias curtas (implicantes) em vez de atribuições totais. Nestes contextos, variáveis não atribuídas atuam como verdadeiros "não importa", e frequentemente apenas um subconjunto de variáveis (variáveis visíveis) é semanticamente relevante, enquanto outras servem como suporte oculto.

Embora solvers SAT modernos calculem eficientemente atribuições satisfatórias totais, a derivação de implicantes curtos tipicamente requer chamadas repetidas ao SAT ou pós-processamento dedicado. Da mesma forma, formulações SAT-para-Ising/QUBO padrão são inerentemente limitadas: elas mapeiam fórmulas CNF para funções de energia quadráticas onde os estados fundamentais correspondem a atribuições totais. O modelo Ising/QUBO atribui um valor a cada spin, carecendo de uma representação nativa para variáveis "não atribuídas". Consequentemente, o cálculo de implicantes curtos historicamente foi deixado para algoritmos externos, em vez de ser capturado dentro do próprio modelo de otimização quadrática.

2. Metodologia

Os autores propõem um framework de otimização unificado que suporta nativamente atribuições parciais de três valores (Verdadeiro, Falso, Não Atribuído) dentro de um modelo quadrático Ising/QUBO.

2.1 Representação de Dupla Polaridade

Para representar variáveis não atribuídas, o framework introduz uma codificação de dupla polaridade. Para cada variável proposicional $A_i$, dois spins binários $(p_i, n_i)$ são utilizados:

• $(1, 0) \implies A_i = \top$
• $(0, 1) \implies A_i = \bot$
• $(0, 0) \implies A_i$ está não atribuído (não importa)
• $(1, 1) \implies$ Inconsistente (proibido)

Uma penalidade de consistência semântica $M \cdot p_i n_i$ é adicionada para proibir o estado inconsistente.

2.2 Codificação de Cláusulas

As cláusulas são codificadas usando funções de penalidade quadráticas padrão. Para uma cláusula $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$, os literais são mapeados para seus spins de polaridade correspondentes. Para manter a forma quadrática, uma variável auxiliar $c_k$ é introduzida para capturar a condição onde os dois primeiros literais são falsos. A função de energia penaliza configurações onde todos os literais são falsos (ou seja, todos os spins correspondentes são 0).

2.3 Esparsidade e Função Objetivo

Um termo de esparsidade é adicionado à função de energia: $E_{sparse} = \gamma \sum (p_i + n_i)$. Este termo penaliza spins ativos, enviesando o otimizador para configurações com menos variáveis atribuídas (implicantes mais curtos).
A função de energia total é:
$$E_F = \sum M p_i n_i + \sum E_{cláusula}(k) + \gamma \sum (p_i + n_i)$$

2.4 Regimes de Peso

O artigo estabelece condições teóricas sobre os pesos ($\lambda$ para penalidades de cláusula, $M$ para consistência, $\gamma$ para esparsidade) para garantir a correção. Especificamente, se $\lambda > n\gamma$ e $M > n\gamma$ (onde $n$ é o número de variáveis), os estados fundamentais da função de energia correspondem exatamente a implicantes de cardinalidade mínima.

2.5 Redução e Projeção

• Redução de Implicante: Dada uma atribuição satisfatória total, o framework restringe o espaço de busca fixando os spins de polaridade "oposta" a 0. Isso permite que o otimizador apenas remova literais da atribuição existente, encontrando a sub-atribuição mais curta que permanece um implicante válido.
• Projeção: Para focar em um subconjunto de variáveis visíveis $P$, a penalidade de esparsidade é aplicada apenas às variáveis em $P$. Variáveis ocultas $H$ permanecem não restringidas pela esparsidade, atuando como suporte auxiliar livre. Isso permite que o modelo encontre atribuições curtas sobre $P$ enquanto satisfaz a fórmula via $H$.

3. Contribuições Principais

1. Codificação Nativa de Três Valores: Uma codificação SAT-para-Ising/QUBO que representa nativamente atribuições parciais (Verdadeiro/Falso/Não Atribuído) via semântica de dupla polaridade, eliminando a necessidade de pós-processamento externo para interpretar estados "não atribuídos".
2. Variantes de Objetivo Flexíveis: Formulações QUBO onde a redução de implicante é alcançada por restrições de polaridade e a projeção é alcançada restringindo penalidades de esparsidade a variáveis visíveis, tudo dentro de uma única estrutura fixa de modelo quadrático.
3. Garantias Teóricas: Identificação de regimes de peso específicos ($\lambda > n\gamma, M > n\gamma$) que garantem que os estados fundamentais correspondam a implicantes de cardinalidade mínima. O artigo fornece um critério para reconhecer implicantes válidos diretamente do valor final de energia.
4. Validação Empírica: Uma avaliação usando Recozimento Simulado em fórmulas 3-SAT aleatórias e fórmulas não-CNF, demonstrando a capacidade da codificação de produzir atribuições parciais curtas e alcançar minimalidade através de refinamento iterativo.

4. Resultados Experimentais

Os autores avaliaram a codificação usando Recozimento Simulado (SA) em dois conjuntos de referência:

• 3-SAT Aleatório: Instâncias satisfatíveis com baixa densidade de cláusulas por variável ($m/n = 1.5$).
• Fórmulas Não-CNF: Fórmulas booleanas convertidas para CNF via transformações Tseitin/Plaisted-Greenbaum, criando um cenário projetado com variáveis auxiliares ocultas.

Principais Descobertas:

• Compactação: Em 3-SAT aleatório, a codificação deixa aproximadamente um terço das variáveis não atribuídas em média, enquanto preserva a satisfatibilidade.
• Minimalidade: Embora o SA de base frequentemente encontre atribuições de cardinalidade mínima em instâncias pequenas a médias, as taxas de sucesso diminuem à medida que o tamanho do problema cresce devido a mínimos locais. No entanto, o refinamento iterativo (congelando a melhor solução e reexecutando o SA para reduzir ainda mais) melhora significativamente os resultados.
• Minimalidade vs. Cardinalidade Mínima: O refinamento iterativo alcança minimalidade por inclusão (implicantes primos) com alta probabilidade. Alcançar cardinalidade mínima (tamanho global mínimo) é mais difícil, mas frequentemente observado, particularmente em benchmarks não-CNF onde a estrutura permite completamentos ocultos uniformes.
• Cenário Projetado: No modo projetado, o método recupera com sucesso atribuições de cardinalidade mínima sobre variáveis visíveis, mesmo com uma alta proporção de variáveis auxiliares ocultas (65–70% do total de variáveis).

5. Significado e Alegações

O artigo afirma que este framework oferece uma abordagem de otimização unificada para o cálculo de atribuições parciais curtas, substituindo a necessidade de sub-rotinas de redução externas em pipelines de AllSAT ou explicação.

• Significado Teórico: Ele preenche a lacuna entre a natureza de "atribuição total" dos modelos Ising e os requisitos de "atribuição parcial" de muitas tarefas de raciocínio, introduzindo uma representação de dupla polaridade com regimes de peso prováveis para minimalidade.
• Significado Prático: A codificação serve como um "substituto direto" para etapas de redução em fluxos de trabalho existentes. Os autores enfatizam que a abordagem é robusta sob backends de otimização genéricos (como Recozimento Simulado) e não requer hardware especializado para demonstrar validade semântica, embora notem que recozidores quânticos ou máquinas Ising especializadas poderiam potencialmente produzir melhores resultados.
• Limitações: Os autores modestamente reconhecem que, embora a codificação garanta estados fundamentais de cardinalidade mínima teoricamente, otimizadores heurísticos podem ficar presos em mínimos locais. Além disso, no cenário projetado, a codificação impõe uma "testemunha uniforme" (uma única atribuição oculta para todas as completudes visíveis), que é um requisito mais estrito do que a semântica padrão de implicantes projetados, embora os autores argumentem que isso vale para muitas conversões práticas não-CNF.

O trabalho posiciona-se como uma validação semântica de codificações quadráticas para raciocínio parcial, demonstrando que, com ajuste adequado de parâmetros e refinamento iterativo, modelos Ising/QUBO podem calcular efetivamente implicantes mínimos e de cardinalidade mínima.