A Top-Down Tree Model Counter for Quantified Boolean Formulas

A Top-Down Tree Model Counter for Quantified Boolean Formulas

Florent Capelli, Jean-Marie Lagniez, Andreas Plank, Martina Seidl

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Main Track. Pages 1853-1861. https://doi.org/10.24963/ijcai.2024/205

This paper addresses the challenge of solution counting for Quantified Boolean Formulas (QBFs), a task distinct from the well-established model counting problem for SAT (\#SAT). Unlike SAT, where models are straightforward assignments to Boolean variables, QBF solution counting involves tree models that capture dependencies among variables within different quantifier blocks. We present a comprehensive top-down tree model counter capable of handling diverse satisfiable QBF formulas. Emphasizing the critical role of the branching heuristic, which must consider variables in the correct order according to quantification blocks, we further demonstrate the importance of addressing connected components, free variables, and caching. Experimental results indicate that our proposed approach for counting tree models of QBF formulas is highly efficient in practice, surpassing existing state-of-the-art methods designed for this specific purpose.
Keywords:
Constraint Satisfaction and Optimization: CSO: Satisfiabilty
Constraint Satisfaction and Optimization: CSO: Solvers and tools