Expansion-based QBF solving versus Q-resolution

This article introduces and studies a proof system ∀Exp+Res that enables us to refute quantified Boolean formulas (QBFs). The system ∀Exp+Res operates in two stages: it expands all universal variables through conjunctions and refutes the result by propositional resolution. This approach contrasts with the Q-resolution calculus, which enables refuting QBFs by rules similar to propositional resolution. In practice, Q-resolution enables producing proofs from conflict-driven DPLL-based QBF solvers. The system ∀Exp+Res can on the other hand certify certain expansion-based solvers. So a natural question is to ask which of the systems, Q-resolution and ∀Exp+Res, is more powerful? The article gives several partial responses to this question. On the positive side, we show that ∀Exp+Res can p-simulate tree Q-resolution. On the negative side, we show that ∀Exp+Res does not p-simulate unrestricted Q-resolution. In the favor of ∀Exp+Res we show that ∀Exp+Res is more powerful than a certain fragment of Q-resolution, which is important for DPLL-based QBF solving.

Authors

• Mikoláš Janota CTU
• Joao Marques-Silva ICREA, Universitat de Lleida

Keywords

• Quantified Boolean formula
• Proof theory
• Expansion
• Q-resolution
• SAT