Solving QBF by Clause Selection

Resumo Técnico: Resolvendo QBF por Seleção de Cláusulas

Declaração do Problema
O artigo aborda o problema de resolver Fórmulas Booleanas Quantificadas (QBFs), especificamente aquelas em Forma Normal Conjuntiva Prenex (PQCNF). Decidir a validade de QBFs é um problema PSPACE-completo, abrangendo aplicações como verificação de modelos, planejamento e jogos de dois jogadores. Embora a resolução de SAT tenha tido grande sucesso, a resolução de QBF permanece desafiadora. As abordagens existentes geralmente se dividem em duas categorias: aprendizado baseado em conflito/solução (extensão do aprendizado de cláusulas de SAT) e métodos baseados em expansão (conversão de QBFs em problemas de SAT). Os autores propõem uma abordagem inovadora que aproveita a dualidade de conjuntos de cobertura (hitting sets) e a enumeração implícita de conjuntos de cobertura para resolver QBFs.

Metodologia
A metodologia central, denominada QESTO (Qbf clausE SelecTion sOlver), trata a resolução de QBF como um jogo entre um jogador universal e um jogador existencial. O algoritmo opera selecionando e desselecionando iterativamente cláusulas em diferentes níveis de quantificação usando um resolvedor de SAT como um oráculo.

1. QBF de Dois Níveis ($\forall \exists$):
   Os autores desenvolvem primeiro um algoritmo para fórmulas com dois níveis de quantificação. Eles estabelecem um vínculo entre a resolução de $\forall X \exists Y. \phi$ e a enumeração de conjuntos de cobertura implícitos.

   • Mecanismo: O algoritmo mantém um conjunto de variáveis de seleção $s_C$ para cada cláusula $C$. Um resolvedor de SAT é usado para encontrar um conjunto de cláusulas $S$ que podem ser "selecionadas" (ou seja, seus literais universais podem ser definidos como falsos).
   • Verificação: Se a parte existencial das cláusulas selecionadas for insatisfatível, o jogador universal vence (a fórmula é falsa). Se for satisfatível, o algoritmo aprende com a atribuição satisfatória para bloquear futuras seleções de subconjuntos de cláusulas que foram satisfeitas, efetivamente buscando por um Conjunto Minimalmente Insatisfatível (MUS) da parte existencial restrita por regras universais.
   • Relação com a Teoria: Este processo é mostrado como uma aplicação do princípio de dualidade de conjuntos de cobertura, onde o algoritmo percorre Conjuntos Maximalmente Satisfatíveis (MSSes) para encontrar MUSes.

2. QBF Geral (Prefixos Arbitrários):
   A abordagem é generalizada para prefixos de quantificadores arbitrários ($Q_1 X_1 \dots Q_n X_n. \phi$).

   • Visão Teoria dos Jogos: O algoritmo simula um jogo com $n$ rodadas. Em cada nível $i$, o jogador $Q_i$ seleciona ou desseleciona cláusulas com base em regras específicas:
     • Uma cláusula pode ser selecionada no nível $k$ apenas se foi selecionada em todos os níveis anteriores e todos os seus literais no nível $k$ forem definidos como falsos.
     • Uma cláusula pode ser desselecionada se foi desselecionada anteriormente ou se um literal no nível $k$ for definido como verdadeiro.
   • Lógica de Seleção de Cláusulas: O algoritmo mantém condições $C_i$ para cada nível que bloqueiam escolhas que levam à perda para o jogador atual.
   • Análise de Conflito: Quando uma condição torna-se insatisfatível (indicando que um jogador perdeu), o algoritmo realiza uma "análise de perda" usando a cláusula de conflito final do resolvedor de SAT.
     • Perda Existencial: Se o jogador existencial perde, o algoritmo identifica um conjunto de cláusulas selecionadas que causam insatisfatibilidade e retrocede ao nível de quantificação mais alto de um literal existencial dentro dessas cláusulas para forçar uma desseleção.
     • Perda Universal: Se o jogador universal perde (todas as cláusulas deselecionadas), o algoritmo retrocede ao nível mais alto onde um jogador universal poderia ter evitado a desseleção.
   • Aprendizado: O algoritmo aprende novas restrições (cláusulas) para evitar que a mesma configuração de perda ocorra novamente, de forma semelhante ao aprendizado impulsionado por conflito em SAT, mas ancorado nas variáveis de seleção.

Principais Contribuições

1. Algoritmo Inovador (QESTO): O artigo introduz o QESTO, um resolvedor de QBF que usa um resolvedor de SAT como um oráculo de caixa preta para selecionar ou desselecionar cláusulas em cada nível de quantificação.
2. Vínculo Teórico com Conjuntos de Cobertura: Estabelece uma conexão formal entre a resolução de QBF e a enumeração de conjuntos de cobertura implícitos, generalizando o princípio de dualidade de conjuntos de cobertura (tipicamente usado para computação de MUS e MaxSAT) para o domínio PSPACE.
3. Conexão com CEGAR: A variante de dois níveis é vinculada a abordagens de Refinamento de Abstração Guiado por Contraexemplo (CEGAR), especificamente o AReQS, embora a generalização (QESTO) difira significativamente do RAReQS ao evitar a introdução de novas variáveis e manter um número fixo de resolvedores.
4. Vantagem de Engenharia: A abordagem depende inteiramente de resolvedores de SAT existentes. Se um melhor resolvedor de SAT for desenvolvido, ele pode ser diretamente substituído na implementação sem modificar a lógica do QBF.

Resultados Experimentais
Os autores implementaram um protótipo em C++ usando MiniSat 2.2 e o avaliaram no conjunto de benchmarks QBFLIB (2014) e na trilha 2QBF (2010).

• Benchmarks 2QBF: O QESTO resolveu o maior número de instâncias (53 de 65), superando o DepQBF (30) e o GhostQ (43). Ficou muito próximo do AReQS (52), o que é esperado dada a sua relação teórica.
• Benchmarks QBFLIB: O GhostQ (um resolvedor não-CNF) dominou os resultados (137 instâncias), seguido pelo QESTO (133). DepQBF e RAReQS resolveram 128 e 129 instâncias, respectivamente.
• Observação: Os resultados sugerem que, embora o QESTO seja competitivo e robusto, representar problemas QBF estritamente em CNF pode ser uma limitação em comparação com abordagens não-CNF como o GhostQ.

Significância e Alegações
O artigo afirma que o QESTO representa uma abordagem inovadora para a resolução de QBF que é tanto teoricamente significativa quanto praticamente competitiva.

• Teórica: Estende o princípio de dualidade de conjuntos de cobertura de NP (MUS/MSS) para PSPACE (QBF), fornecendo uma nova perspectiva sobre a estrutura do problema.
• Prática: O algoritmo é "competitivo com, e muitas vezes supera, o estado da arte" em domínios específicos (particularmente 2QBF).
• Modéstia: Os autores reconhecem que sua abordagem baseada em CNF foi superada pelo resolvedor não-CNF GhostQ no conjunto geral QBFLIB. Eles afirmam explicitamente que trabalhos futuros devem investigar a aplicação do QESTO a fórmulas não-CNF e a incorporação de otimizações como literais puros ou dependências de variáveis. Eles não alegam que o QESTO é o estado da arte absoluto para todas as instâncias de QBF, mas sim uma alternativa robusta e inovadora que une diferentes paradigmas de resolução.