Document Open Access Logo

Tractable QBF by Knowledge Compilation

Authors Florent Capelli, Stefan Mengel

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2019.18.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • QBF
  • knowledge compilation
  • parameterized algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We generalize several tractability results concerning the tractability of Quantified Boolean Formulas (QBF) with restricted underlying structure. To this end, we introduce a notion of width for structured DNNF which are a class of Boolean circuits heavily studied in knowledge compilation, a subarea of artificial intelligence. We then show that structured DNNF allow quantifier elimination with a size blow-up depending only on the width of the DNNF and not its size. Using known algorithms transforming restricted CNF-formulas into deterministic DNNF, we apply this result to generalize several results for counting and decision on QBF. We also complement these results with lower bounds that show that our definitions and results are essentially optimal in several senses.

Cite As Get BibTex

Florent Capelli and Stefan Mengel. Tractable QBF by Knowledge Compilation. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.STACS.2019.18

Author Details

Florent Capelli
  • Université de Lille, Inria, UMR 9189 - CRIStAL - Centre de Recherche en Informatique Signal et Automatique de Lille, F-59000 Lille, France
Stefan Mengel
  • CNRS, CRIL UMR 8188, Lens, France

Funding

This work was partially supported by the French Agence Nationale de la Recherche, AGGREG project reference ANR-14-CE25-0017-01.

Acknowledgements

The authors would like to thank Mikaël Monet for helpful comments on an early version of this paper.

References

  1. Bernhard Bliem, Sebastian Ordyniak, and Stefan Woltran. Clique-Width and Directed Width Measures for Answer-Set Programming. In Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke Hüllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen, editors, ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1105-1113. IOS Press, 2016. URL: http://dx.doi.org/10.3233/978-1-61499-672-9-1105.
  2. Beate Bollig and Ingo Wegener. Asymptotically Optimal Bounds for OBDDs and the Solution of Some Basic OBDD Problems. J. Comput. Syst. Sci., 61(3):558-579, 2000. URL: http://dx.doi.org/10.1006/jcss.2000.1733.
  3. Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. On Compiling CNFs into Structured Deterministic DNNFs. In Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, volume 9340 of Lecture Notes in Computer Science, pages 199-214. Springer, 2015. Google Scholar
  4. Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Knowledge Compilation Meets Communication Complexity. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages 1008-1014. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/147.
  5. Simone Bova and Stefan Szeider. Circuit Treewidth, Sentential Decision, and Query Compilation. In Emanuel Sallinger, Jan Van den Bussche, and Floris Geerts, editors, Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2017, Chicago, IL, USA, May 14-19, 2017, pages 233-246. ACM, 2017. URL: http://dx.doi.org/10.1145/3034786.3034787.
  6. Johann Brault-Baron, Florent Capelli, and Stefan Mengel. Understanding Model Counting for beta-acyclic CNF-formulas. In 32nd International Symposium on Theoretical Aspects of Computer Science, pages 143-156, 2015. Google Scholar
  7. Florent Capelli and Stefan Mengel. Knowledge Compilation, Width and Quantification. CoRR, abs/1807.04263, 2018. URL: http://arxiv.org/abs/1807.04263.
  8. Hubie Chen. Quantified Constraint Satisfaction and Bounded Treewidth. In Ramon López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, pages 161-165, 2004. Google Scholar
  9. Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001. URL: http://dx.doi.org/10.1145/502090.502091.
  10. Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 819-826. IJCAI/AAAI, 2011. URL: http://dx.doi.org/10.5591/978-1-57735-516-8/IJCAI11-143.
  11. Adnan Darwiche and Pierre Marquis. A Knowledge Compilation Map. J. Artif. Intell. Res., 17:229-264, 2002. URL: http://dx.doi.org/10.1613/jair.989.
  12. Wolfgang Dvorák, Stefan Szeider, and Stefan Woltran. Reasoning in Argumentation Frameworks of Bounded Clique-Width. In Pietro Baroni, Federico Cerutti, Massimiliano Giacomin, and Guillermo Ricardo Simari, editors, Computational Models of Argument: Proceedings of COMMA 2010, Desenzano del Garda, Italy, September 8-10, 2010., volume 216 of Frontiers in Artificial Intelligence and Applications, pages 219-230. IOS Press, 2010. URL: http://dx.doi.org/10.3233/978-1-60750-619-5-219.
  13. Andrea Ferrara, Guoqiang Pan, and Moshe Y. Vardi. Treewidth in Verification: Local vs. Global. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: http://dx.doi.org/10.1007/11591191_34.
  14. Johannes Klaus Fichte, Markus Hecher, Michael Morak, and Stefan Woltran. Exploiting Treewidth for Projected Model Counting and Its Limits. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 165-184. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-319-94144-8_11.
  15. Eldar Fischer, Johann A. Makowsky, and Elena V. Ravve. Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Applied Mathematics, 156(4):511-529, 2008. URL: http://dx.doi.org/10.1016/j.dam.2006.06.020.
  16. Georg Gottlob, Reinhard Pichler, and Fang Wei. Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artif. Intell., 174(1):105-132, 2010. URL: http://dx.doi.org/10.1016/j.artint.2009.10.003.
  17. Michael Lampis, Stefan Mengel, and Valia Mitsou. QBF as an alternative to courcelle’s theorem. CoRR, abs/1805.08456, 2018. accepted for SAT'18. URL: http://arxiv.org/abs/1805.08456.
  18. Michael Lampis and Valia Mitsou. Treewidth with a Quantifier Alternation Revisited. In Daniel Lokshtanov and Naomi Nishimura, editors, 12th International Symposium on Parameterized and Exact Computation, IPEC 2017, September 6-8, 2017, Vienna, Austria, volume 89 of LIPIcs, pages 26:1-26:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.IPEC.2017.26.
  19. Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider. Model Counting for CNF Formulas of Bounded Modular Treewidth. Algorithmica, 76(1):168-194, 2016. Google Scholar
  20. Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider. Model Counting for CNF Formulas of Bounded Modular Treewidth. Algorithmica, 76(1):168-194, 2016. URL: http://dx.doi.org/10.1007/s00453-015-0030-x.
  21. Knot Pipatsrisawat and Adnan Darwiche. New Compilation Languages Based on Structured Decomposability. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 517-522. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-082.php.
  22. Thammanit Pipatsrisawat and Adnan Darwiche. A Lower Bound on the Size of Decomposable Negation Normal Form. In Maria Fox and David Poole, editors, Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press, 2010. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1856.
  23. S. Hortemo Sæther, J.A. Telle, and M. Vatshelle. Solving MaxSAT and #SAT on Structured CNF Formulas. In Theory and Applications of Satisfiability Testing, pages 16-31, 2014. Google Scholar
  24. M. Samer and S. Szeider. Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  25. Martin Sauerhoff. Approximation of boolean functions by combinatorial rectangles. Theor. Comput. Sci., 1-3(301):45-78, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00568-6.
  26. Friedrich Slivovsky and Stefan Szeider. Model Counting for Formulas of Bounded Clique-Width. In Leizhen Cai, Siu-Wing Cheng, and Tak Wah Lam, editors, Algorithms and Computation - 24th International Symposium, ISAAC 2013, Hong Kong, China, December 16-18, 2013, Proceedings, volume 8283 of Lecture Notes in Computer Science, pages 677-687. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-45030-3_63.
  27. Stefan Szeider. On fixed-parameter tractable parameterizations of SAT. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability, 6th International Conference, volume 2919 of LNCS, pages 188-202. Springer, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact