Metraipolis › archive › dc_fc1122ed6544

On Knowledge Compilation Languages for QBFs — arXiv:2610.20842

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.20842
License (as archived): CC0-1.0
Archived: 2026-10-16T10:40:27.896Z
SHA-256 of the archived text: 60ce4b182ec06e7a71df43a8c39e11d1342be7b46bd911aa6226f6b5c58251a6
Stable URL of this page: https://metraipolis.com/documento/dc_fc1122ed6544

How to cite

On Knowledge Compilation Languages for QBFs — arXiv:2610.20842 — arXiv (en), https://arxiv.org/abs/2610.20842 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_fc1122ed6544 (Metraipolis archive dc_fc1122ed6544, sha256 60ce4b182ec06e7a71df43a8c39e11d1342be7b46bd911aa6226f6b5c58251a6)

BibTeX

@misc{dcfc1122ed6544,
  title = {On Knowledge Compilation Languages for QBFs — arXiv:2610.20842},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.20842},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_fc1122ed6544; sha256 60ce4b182ec06e7a71df43a8c39e11d1342be7b46bd911aa6226f6b5c58251a6},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.20842. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

In this work, we design knowledge compilation languages for quantified Boolean formulas (QBFs), with a particular focus on model counting. We introduce various languages in increasing order of their power of representation, starting from a simple tree-based structure, and extending it to DAGs for a more efficient representation. We study the power and limitations of each language. We also show that QBF queries such as model counting and MaxQBF are easy to handle in all these languages. These languages naturally lead to various static proof systems for the #QBF problem, the model-counting version of the QBF problem. We compare these systems with one another and with a recently introduced line-based #QBF-system called Q-MICE (Chede, Chew, Krishan and Shukla, SAT `26). We show that a minor extension of the Q-MICE system efficiently simulates all these static proof systems, and is in fact exponentially stronger than each of them. We also initiate the implementation of a solver based on these languages. The solver compiles a representation of an input QBF in the proposed tree-like language, which is subsequently used for model counting. This is the first knowledge compilation based solver for #QBF which can handle QBFs with doubly exponential model counts as well. Experimentally, we compare its performance with the state-of-the-art #QBF-solver d4-QBF which works well for QBFs with small model counts.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv cs.CC, nuovi lavori del giorno).
Categorie arXiv: Computational Complexity (cs.CC).
Pagina del lavoro: https://arxiv.org/abs/2610.20842 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T08:53:47.654Z dalla pagina https://arxiv.org/list/cs.CC/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).