On Proof Systems for #QBF

Título: Sobre Sistemas de Prova para #QBF

Enunciado do Problema
O artigo aborda o problema #QBF, que envolve computar o número de estratégias vencedoras para o jogador existencial em uma Fórmula Booleana Quantificada (QBF). Este problema é identificado como #PSPACE-completo, tornando-o computacionalmente mais difícil que o problema análogo #SAT (contagem de modelos para fórmulas proposicionais), onde o número de soluções é, no máximo, exponencial. Em contraste, o número de estratégias vencedoras em #QBF pode ser duplamente exponencial. Embora sistemas de prova para #SAT (ex: KCPS, CPOG, CLIP, MICE) e para QBF (ex: Q-Res, ∀Exp) tenham sido estudados, havia uma carência de sistemas de prova dedicados para o problema geral #QBF capazes de certificar a contagem de estratégias vencedoras. Solvers existentes como d4-QBF e qCounter existem, mas carecem de um framework formal de complexidade de prova para certificação.

Metodologia
Os autores estendem conceitos de ambos os sistemas de prova de QBF e de sistemas de prova de #SAT para projetar novos sistemas de prova para #QBF. Eles exploram três abordagens distintas:

1. Sistema Ingênuo (Naive System): Um sistema rudimentar que enumera todas as $k$ estratégias vencedoras. Ele certifica a contagem provando a correção de cada estratégia (via provas de tautologia de funções de Skolem), provando a distinção das estratégias (via atribuições de testemunhas) e provando a não existência de quaisquer outras estratégias (via uma codificação de QBF falsa). Os autores observam que este sistema sofre de limites inferiores triviais quando o número de estratégias é duplamente exponencial.
2. Sistema Baseado em Expansão (∀Exp+MICE): Esta abordagem adapta a regra de ∀-expansão usada em solving de QBF. Ela expande semanticamente a QBF sobre todas as possíveis atribuições para variáveis universais, transformando o problema #QBF em um problema #SAT. A CNF resultante é então processada pelo sistema de prova de #SAT MICE. Os autores argumentam que este sistema inerentemente requer tamanho exponencial em relação ao número de variáveis universais porque deve expandir todas as atribuições universais para preservar a contagem de modelos.
3. Sistema Baseado em Linhas (Q-MICE): A principal contribuição é a proposta do Q-MICE (Quantified Model-counting Induction by Claim Extension). Inspirado no sistema MICE para #SAT, o Q-MICE é um sistema de prova baseado em linhas onde cada linha é uma alegação da forma $(Q.F, A, c)$.
   • $Q.F$: Uma QBF verdadeira.
   • $A$: Uma estratégia parcial consistindo de funções de Skolem para um subconjunto de variáveis existenciais.
   • $c$: O número de maneiras de estender $A$ em estratégias vencedoras completas.
   • Regras de Inferência: O Q-MICE utiliza três regras principais:
     • Regra de Axioma: Deriva alegações para QBFs restritas onde a matriz é uma tautologia, permitindo a contagem combinatória direta de extensões.
     • Regras de Composição: Permitem combinar ou simplificar alegações. Composição-a soma estratégias completas distintas; Composição-b remove restrições de estratégia quando a unicidade é provada; Composição-c combina alegações onde as estratégias diferem apenas em variáveis específicas, desde que uma prova de "ausência de modelos" certifique que não existem outras estratégias.
     • Regra de Junção (Join Rule): Combina duas alegações que diferem apenas por uma restrição em uma variável universal, multiplicando suas contagens, desde que a estrutura da árvore de atribuição permita isso (grafos de caminho).

Principais Contribções e Resultados

• Formalização do Q-MICE: O artigo define o Q-MICE e prova que ele é som e completo (Teorema 16). Ele é verificável em tempo polinomial.
• Separação Exponencial: Os autores demonstram que o Q-MICE é exponencialmente mais forte que tanto o sistema ingênuo quanto o sistema ∀Exp+MICE (Teorema 17).
  • Família XOR-PAIRS: Eles introduzem uma versão quantificada da fórmula proposicional XOR-PAIRS. Enquanto esta família exige provas superpolinomiais (exponenciais) em ∀Exp+MICE devido à necessidade de expandir variáveis universais, o Q-MICE fornece uma prova de comprimento constante e tamanho polinomial, utilizando as regras de Axioma e Composição-b.
  • Família QBF Afim Indexada: Eles constroem uma família de QBFs que representam um processo de criptografia simples. Esta família possui $2^n$ estratégias vencedoras, exigindo provas exponenciais tanto no sistema ingênuo quanto no ∀Exp+MICE. O Q-MICE lida com isso através de uma prova de comprimento linear e tamanho polinomial, aplicando iterativamente as regras de composição e junção.
• Análise Estrutural: O artigo destaca que sistemas baseados em expansão sofrem de fraquezas estruturais inerentes (explosão exponencial) ao lidar com variáveis universais, enquanto o Q-MICE intercala o tratamento de quantificadores com a contagem para manter a eficiência.

Significância e Alegações
O artigo afirma que a existência de sistemas de prova como o Q-MICE é crucial para avançar a teoria do #QBF e para certificar a correção de solvers de #QBF, uma área que se encontra em seus estágios iniciais. Ao fornecer um framework para certificar contagens de modelos sem enumerar todas as estratégias, o Q-MICE oferece um caminho para solvers mais robustos e verificáveis.

Os autores observam modestamente que, embora o Q-MICE seja poderoso, ele ainda não incorpora as regras de decomposição encontradas em solvers de estado da arte como o d4-QBF, embora sugiram que isso possa ser adicionado como uma regra de inferência modular. Eles também identificam problemas abertos, incluindo o estabelecimento de limites inferiores genuínos para o Q-MICE (conjecturando que o XOR-PAIRS proposicional pode ser difícil para ele, embora isso ainda não seja um limite inferior provado) e a extensão de outros sistemas de prova de #SAT (CPOG, CLIP, KCPS) para o domínio do #QBF. O artigo não propõe novos solvers experimentais, mas foca estritamente na complexidade de prova teórica e na separação desses sistemas.