Knowledge compilation languages improve counting solutions for quantified logic formulas
On Knowledge Compilation Languages for QBFs
Computational Complexity
Summary
Counting the number of solutions for complex logical formulas that include functions like 'for all' and 'there exists' can be very difficult. The authors design new ways to represent these formulas that make counting easier and more efficient. They compare these new methods to older ones and show that a slight improvement to a recent approach can do even better than all of these. They also started building a solver tool using these ideas, which can handle very large problem cases better than some current solvers.
What this means in practice
- •For formal verification engineers: Use the new solver to efficiently count models of QBF formulas in hardware and software verification tasks with complex quantifier structures.
- •For tool developers for automated reasoning: Incorporate the proposed knowledge compilation languages into reasoning tools to improve efficiency and scalability of counting solutions for quantified logic problems.
Authors
Sravanthi Chede, Vaibhav Krishan, Anil Shukla
Abstract
In this work, we design knowledge compilation languages for quantified Boolean formulas (QBFs), with a particular focus on model counting. We introduce various languages in increasing order of their power of representation, starting from a simple tree-based structure, and extending it to DAGs for a more efficient representation. We study the power and limitations of each language. We also show that QBF queries such as model counting and MaxQBF are easy to handle in all these languages. These languages naturally lead to various static proof systems for the #QBF problem, the model-counting version of the QBF problem. We compare these systems with one another and with a recently introduced line-based #QBF-system called Q-MICE (Chede, Chew, Krishan and Shukla, SAT `26). We show that a minor extension of the Q-MICE system efficiently simulates all these static proof systems, and is in fact exponentially stronger than each of them. We also initiate the implementation of a solver based on these languages. The solver compiles a representation of an input QBF in the proposed tree-like language, which is subsequently used for model counting. This is the first knowledge compilation based solver for #QBF which can handle QBFs with doubly exponential model counts as well. Experimentally, we compare its performance with the state-of-the-art #QBF-solver d4-QBF which works well for QBFs with small model counts.