Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking

Resumo Técnico: Esquemas de Dependência Fortes (D)QBF via Camadas Puras com Aplicações na Verificação de Provas

Declaração do Problema
A certificação para Fórmulas Booleanas Quantificadas (QBF) e Fórmulas Booleanas Quantificadas com Dependência (DQBF) permanece um desafio significativo. Embora pesquisas recentes em complexidade de provas tenham demonstrado que a regra "Extensão Independente" (IndExt) permite que o sistema de provas IndExtQURes simule em tempo polinomial (p-simule) a vasta maioria das técnicas existentes de QBF e DQBF, o próprio IndExtQURes ainda não é um formato de certificação prático. Por outro lado, formatos práticos como QRAT (Tautologia Assimétrica de Resolução Quantificada) e sua generalização DQBF, DQRAT (Tautologia Assimétrica de Resolução Quantificada com Dependência), carecem da força teórica para p-simular o IndExtQURes. Especificamente, o DQRAT, que depende do esquema de dependência de caminho de resolução reflexivo ($D_{rrs}$), não foi provado como equivalente em poder ao IndExtQURes, deixando uma lacuna entre a otimalidade teórica e a certificação prática.

Metodologia
Os autores abordam essa lacuna introduzindo um novo esquema de dependência chamado $D_{\forall pure}$ (Esquema de Dependência Universal Pura). Este esquema baseia-se no conceito de "caminhos puros", que restringe os caminhos de resolução entre literais universais e existenciais. Diferentemente do caminho de resolução reflexivo padrão ($D_{rrs}$), o $D_{\forall pure}$ exclui caminhos de resolução de um literal universal $u$ para um literal existencial $x$ se o caminho for meramente uma extensão de um caminho de $\bar{u}$ para $x$. Isso garante que apenas dependências mínimas e necessárias sejam retidas.

A metodologia envolve três componentes principais:

1. Definição e Corretude: Os autores definem formalmente o $D_{\forall pure}$ usando construções de ponto fixo em conjuntos de cláusulas e literais. Eles provam a corretude semântica deste esquema (Teorema 10), demonstrando que a remoção de dependências espúrias identificadas pelo $D_{\forall pure}$ preserva o valor de verdade da DQBF.
2. Integração em Sistemas de Provas: Os autores integram o $D_{\forall pure}$ no sistema de provas DQRAT, criando um novo sistema denotado como DQRAT+$D_{\forall pure}$. Eles também definem uma regra de redução local, Loc$_{\forall pure}$-Red, que permite a redução direta de cláusulas contendo literais universais sem alterar o prefixo, desde que não existam caminhos puros para cláusulas conflitantes.
3. Análise de Complexidade: O artigo estabelece a relação entre o novo sistema e o IndExtQURes. Os autores provam que o DQRAT+$D_{\forall pure}$ e o IndExtQURes são p-equivalentes (equivalentes em tempo polinomial). Isso é alcançado mostrando que o DQRAT+$D_{\forall pure}$ pode p-simular o IndExtQURes (simulando a regra de Extensão Independente usando o novo esquema de dependência para remover dependências desnecessárias) e que o IndExtQURes pode p-simular o DQRAT+$D_{\forall pure}$.

Principais Contribuições

• Novo Esquema de Dependência ($D_{\forall pure}$): O artigo introduz um esquema de dependência que é estritamente mais forte que o $D_{rrs}$ em contextos específicos (por exemplo, separando LD-Q(Drrs)-Res de LD-Q(D$_{\forall pure}$)-Res) enquanto mantém a verificabilidade em tempo polinomial.
• Equivalência de Sistemas de Provas: A contribuição teórica primária é a prova de que o DQRAT+$D_{\forall pure}$ é p-equivalente ao IndExtQURes. Isso implica que o DQRAT+$D_{\forall pure}$ pode p-simular todos os principais sistemas de provas de QBF e DQBF que o IndExtQURes pode, incluindo QRAT, G e várias regras de esquema de dependência.
• Extração de Estratégia: Os autores mostram que o $D_{\forall pure}$ é um esquema de dependência "normal", o que permite a extração de estratégias em tempo polinomial na Resolução-Q de Longa Distância (LD-Q-Res). Este resultado apoia a integração correta do $D_{\forall pure}$ em solucionadores como o Qute.
• Implementação: Os autores implementaram um verificador de provas protótipo, DQRAT-check, que suporta o formato DQRAT+$D_{\forall pure}$. Eles também estenderam o solucionador Qute para utilizar o $D_{\forall pure}$ para aprendizado de cláusulas.

Resultados

• Teórico: O artigo demonstra que o $D_{\forall pure}$ permite a remoção de dependências que o $D_{rrs}$ não consegue, especificamente em casos envolvendo fórmulas de paridade "ponteadas", onde o $D_{rrs}$ falha em detectar independência, mas o $D_{\forall pure}$ tem sucesso.
• Experimental (Verificação de Provas): O verificador protótipo foi testado em benchmarks do QBFEval 2022 e fórmulas criadas (incluindo os exemplos do artigo). O verificador verificou com sucesso as provas. Os autores notam que a extração e conversão de provas do QRP (formato interno do Qute) para DQRAT representam 97% do tempo de verificação, enquanto o próprio verificador DQRAT representa apenas 3%.
• Experimental (Resolução): Quando integrado ao solucionador Qute, o $D_{\forall pure}$ mostrou promessa nos benchmarks do QBFEval 2020, reduzindo o tempo de computação de dependência em 7 vezes e encontrando o dobro de pares independentes em comparação com o $D_{rrs}$. No entanto, nos benchmarks mais recentes do QBFEval 2022, o $D_{\forall pure}$ não detectou novas independências, e a sobrecarga não melhorou o número de instâncias resolvidas ou as pontuações PAR2.

Significância
O artigo afirma que sua principal significância reside em preencher a lacuna entre a força teórica das provas e os formatos de certificação práticos. Ao mostrar que uma modificação simples na estrutura existente do DQRAT (adicionando a regra $D_{\forall pure}$) produz um sistema p-equivalente ao poderoso IndExtQURes, os autores fornecem um caminho para um padrão de certificação unificado e forte tanto para QBF quanto para DQBF. Isso evita a necessidade de provar p-simulações para cada sistema de provas individual contra o IndExtQURes, confiando, em vez disso, na transitividade da equivalência entre DQRAT+$D_{\forall pure}$ e IndExtQURes. Além disso, o trabalho fornece uma implementação concreta (DQRAT-check) e demonstra a viabilidade de integrar esses esquemas de dependência fortes na infraestrutura de resolução existente, abrindo caminho para uma certificação mais robusta em futuros solucionadores de DQBF.