Document Open Access Logo

Small Resolution Proofs for QBF using Dependency Treewidth

Authors Eduard Eiben, Robert Ganian, Sebastian Ordyniak

PDF
Thumbnail PDF

File

LIPIcs.STACS.2018.28.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Eduard Eiben
Robert Ganian
Sebastian Ordyniak

Cite As Get BibTex

Eduard Eiben, Robert Ganian, and Sebastian Ordyniak. Small Resolution Proofs for QBF using Dependency Treewidth. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.STACS.2018.28

Abstract

In spite of the close connection between the evaluation of quantified Boolean formulas (QBF) and propositional satisfiability (SAT), tools and techniques which exploit structural properties of SAT instances are known to fail for QBF. This is especially true for the structural parameter treewidth, which has allowed the design of successful algorithms for SAT but cannot be straightforwardly applied to QBF since it does not take into account the interdependencies between quantified variables.

In this work we introduce and develop dependency treewidth, a new structural parameter based on treewidth which allows the efficient solution of QBF instances. Dependency treewidth pushes the frontiers of tractability for QBF by overcoming the limitations of previously introduced variants of treewidth for QBF. We augment our results by developing algorithms for computing the decompositions that are required to use the parameter.

Subject Classification

Keywords
  • QBF
  • treewidth
  • fixed parameter tractability
  • dependency schemes

Metrics

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

References

  1. Isolde Adler and Mark Weyer. Tree-width for first order formulae. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  2. Albert Atserias and Sergi Oliva. Bounded-width QBF is pspace-complete. J. Comput. Syst. Sci., 80(7):1415-1429, 2014. Google Scholar
  3. Armin Biere and Florian Lonsing. Integrating dependency schemes in search-based QBF solvers. In Theory and Applications of Satisfiability Testing - SAT 2010, volume 6175 of Lecture Notes in Computer Science, pages 158-171. Springer, 2010. Google Scholar
  4. Hans L. Bodlaender. A linear time algorithm for finding tree-decompositions of small treewidth. In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 226-234, 1993. Google Scholar
  5. Florent Capelli. Structural restrictions of CNF-formulas: applications to model counting and knowledge compilation. PhD thesis, Université Paris Diderot, 2016. Google Scholar
  6. Hubie Chen and Víctor Dalmau. Decomposing quantified conjunctive (or disjunctive) formulas. SIAM J. Comput., 45(6):2066-2086, 2016. Google Scholar
  7. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. Google Scholar
  8. M. Davis and H. Putnam. A computing procedure for quantification theory. 7(3):201-215, 1960. Google Scholar
  9. Reinhard Diestel. Graph Theory, 4th Edition, volume 173 of Graduate texts in mathematics. Springer, 2012. Google Scholar
  10. Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer Verlag, 2013. Google Scholar
  11. Uwe Egly, Thomas Eiter, Hans Tompits, and Stefan Woltran. Solving advanced reasoning tasks using quantified boolean formulas. In Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30 - August 3, 2000, Austin, Texas, USA., pages 417-422, 2000. Google Scholar
  12. Eduard Eiben, Robert Ganian, and Sebastian Ordyniak. Using decomposition-parameters for QBF: mind the prefix! In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA., pages 964-970, 2016. Google Scholar
  13. Eduard Eiben, Robert Ganian, and Sebastian Ordyniak. Small resolution proofs for QBF using dependency treewidth. CoRR, abs/1711.02120, 2017. URL: http://arxiv.org/abs/1711.02120.
  14. S. Felsner, V. Raghavan, and J. Spinrad. Recognition algorithms for orders of small width and graphs of small dilworth number. Order, 20(4):351-364, 2003. Google Scholar
  15. Jörg Flum and Martin Grohe. Parameterized Complexity Theory, volume XIV of Texts in Theoretical Computer Science. An EATCS Series. Springer Verlag, Berlin, 2006. Google Scholar
  16. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  17. Hans Kleine Büning and Uwe Bubeck. Theory of quantified boolean formulas. In A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 23, pages 735-760. IOS Press, 2009. Google Scholar
  18. Hans Kleine Büning and Theodor Lettman. Propositional logic: deduction and algorithms. Cambridge University Press, Cambridge, 1999. Google Scholar
  19. T. Kloks. Treewidth: Computations and Approximations. Springer Verlag, Berlin, 1994. Google Scholar
  20. Charles Otwell, Anja Remshagen, and Klaus Truemper. An effective QBF solver for planning problems. In Proceedings of the International Conference on Modeling, Simulation & Visualization Methods, MSV '04 & Proceedings of the International Conference on Algorithmic Mathematics & Computer Science, AMCS '04, June 21-24, 2004, Las Vegas, Nevada, USA, pages 311-316. CSREA Press, 2004. Google Scholar
  21. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  22. Luca Pulina and Armando Tacchella. A structural approach to reasoning with quantified boolean formulas. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 596-602, 2009. Google Scholar
  23. Luca Pulina and Armando Tacchella. An empirical study of QBF encodings: from treewidth estimation to useful preprocessing. Fundam. Inform., 102(3-4):391-427, 2010. Google Scholar
  24. J. Rintanen. Constructing conditional plans by a theorem-prover. J. Artif. Intell. Res., 10:323-352, 1999. Google Scholar
  25. Ashish Sabharwal, Carlos Ansótegui, Carla P. Gomes, Justin W. Hart, and Bart Selman. QBF modeling: Exploiting player symmetry for simplicity and efficiency. In Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, pages 382-395, 2006. Google Scholar
  26. Marko Samer and Stefan Szeider. Backdoor sets of quantified Boolean formulas. Journal of Autom. Reasoning, 42(1):77-97, 2009. Google Scholar
  27. Friedrich Slivovsky and Stefan Szeider. Computing resolution-path dependencies in linear time. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012, volume 7317 of Lecture Notes in Computer Science, pages 58-71. Springer Verlag, 2012. Google Scholar
  28. Friedrich Slivovsky and Stefan Szeider. Quantifier reordering for QBF. J. Autom. Reasoning, 56(4):459-477, 2016. Google Scholar
  29. Friedrich Slivovsky and Stefan Szeider. Soundness of q-resolution with dependency schemes. Theor. Comput. Sci., 612:83-101, 2016. Google Scholar
  30. Daniel A Spielman and Miklós Bóna. An infinite antichain of permutations. Electron. J. Combin, 7:N2, 2000. Google Scholar
  31. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. Google Scholar
  32. Stefan Szeider. On fixed-parameter tractable parameterizations of SAT. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability, 6th International Conference, SAT 2003, Selected and Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 188-202. Springer Verlag, 2004. Google Scholar
  33. Allen Van Gelder. Variable independence and resolution paths for quantified boolean formulas. In Jimmy Lee, editor, Principles and Practice of Constraint Programming - CP 2011, volume 6876 of Lecture Notes in Computer Science, pages 789-803. Springer Verlag, 2011. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact