OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas
Sprache des Vortragstitels:
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 problems of formal verification, synthesis, planning, etc., practical solution counting has not been considered yet.
We present the first practical counter of top-level solutions, i.e., a tool for counting full assignments of the variables in the outermost quantifier. Our tool is able to count such solutions for true and for false formulas.