On Proof Systems for #QBF
2026-06-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study the problem of counting winning strategies for quantified Boolean formulas (#QBF), which is harder than counting solutions for regular Boolean formulas (#SAT). They develop new proof systems specifically for #QBF that help both in theory and in improving solvers. After examining some existing approaches, they identify weaknesses and introduce a new system called Q-MICE, which uses sound rules inspired by a similar #SAT system. Their results show that Q-MICE can handle problems that are difficult for other #QBF methods, proving it to be stronger in certain cases.
Quantified Boolean Formulas (QBF)#QBF problem#SAT problemProof SystemsSkolem FunctionsExpansion RuleQ-MICEMICE proof systemXOR-PAIRS formula
Authors
Sravanthi Chede, Leroy Chew, Vaibhav Krishan, Anil Shukla
Abstract
For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. Apart from a naive system, we study #QBF systems based on the expansion rule of universal variables in QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.