Enumerative Level-2 Solution Counting for Quantified Boolean Formulas

Description

We lift the problem of enumeratively counting solutions to quantified Boolean formulas (QBFs) at the second level. In contrast to the well-explored model counting problem for SAT (#SAT), where models are simply assignments to the Boolean variables of a formula, we are now dealing with tree (counter-)models reflecting the dependencies between the variables of the first and the second quantifier block. It turns out that enumerative counting on the second level only counts disjoint models. We present the—to the best of our knowledge—first approach of counting tree (counter-)models together with a counting tool that exploits state-of-the-art QBF technology. We provide several kinds of benchmarks for testing our implementation and illustrate in several case studies that solution counting provides valuable insights into QBF encodings.

Period	29 Aug 2023
Event title	The 29th International Conference on Principles and Practice of Constraint Programming. CP 2023
Event type	Conference
Location	CanadaShow on map