License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2023.49
URN: urn:nbn:de:0030-drops-190867
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19086/
Go to the corresponding LIPIcs Volume Portal

Plank, Andreas ; Möhle, Sibylle ; Seidl, Martina

Enumerative Level-2 Solution Counting for Quantified Boolean Formulas (Short Paper)

pdf-format:
LIPIcs-CP-2023-49.pdf (0.7 MB)

Abstract

We lift the problem of enumerative solution counting 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 does not give the complete model count. 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.

BibTeX - Entry

@InProceedings{plank_et_al:LIPIcs.CP.2023.49,
  author =	{Plank, Andreas and M\"{o}hle, Sibylle and Seidl, Martina},
  title =	{{Enumerative Level-2 Solution Counting for Quantified Boolean Formulas}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{49:1--49:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19086},
  URN =		{urn:nbn:de:0030-drops-190867},
  doi =		{10.4230/LIPIcs.CP.2023.49},
  annote =	{Keywords: QBF, Second-Level Model Counting}
}

Keywords: QBF, Second-Level Model Counting
Collection: 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)
Issue Date: 2023
Date of publication: 22.09.2023
Supplementary Material: Software: https://qcount.pages.sai.jku.at/l2count

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI