OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas

Counting the solutions of symbolic encodings is an intriguing computational problem with many applications. In the field of propositional satisfiability (SAT) solving, for example, many algorithms and tools have emerged to tackle the counting problem. For quantified Boolean formulas (QBFs), an extension of SAT with quantifiers used to compactly encode and solve problems of formal verification, synthesis, planning, etc., practical solution counting has not been considered yet. We present the first practical counting algorithm for top-level solutions. We prove soundness of our algorithm for true and false formulas and show how to implement it with recent QBF solving technology. Our evaluation of benchmarks from the recent QBF competition gives promising results for this difficult problem.