Knowledge Compilation, Width and Quantification
Florent Capelli, Stefan Mengel

TL;DR
This paper extends tractability results for SAT and #SAT on bounded treewidth CNF formulas to the more complex setting of Quantified Boolean Formulas (QBF), using width notions in OBDD and DNNF representations.
Contribution
It introduces a generalized width concept for structured DNNF, enabling efficient variable projection and model counting for bounded treewidth and quantifier alternation QBFs.
Findings
Counting models of bounded treewidth quantified CNF is fixed-parameter tractable.
Width blow-up during variable projection depends only on width, not size.
Several bounds on width are proven to be optimal.
Abstract
We generalize many results concerning the tractability of SAT and #SAT on bounded treewidth CNF-formula in the context of Quantified Boolean Formulas (QBF). To this end, we start by studying the notion of width for OBDD and observe that the blow up in size while existentially or universally projecting a block of variables in an OBDD only affects its width. We then generalize this notion of width to the more general representation of structured (deterministic) DNNF and give a similar algorithm to existentially or universally project a block of variables. Using a well-known algorithm transforming bounded treewidth CNF formula into deterministic DNNF, we are able to generalize this connection to quantified CNF which gives us as a byproduct that one can count the number of models of a bounded treewidth and bounded quantifier alternation quantified CNF in FPT time. We also give an extensive…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Graph Theory Research · Constraint Satisfaction and Optimization · Formal Methods in Verification
