Document Open Access Logo

QBF Programming with the Modeling Language Bule

Authors Jean Christoph Jung, Valentin Mayer-Eichberger, Abdallah Saffidine

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2022.31.pdf
  • Filesize: 0.8 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Hardware → Theorem proving and SAT solving
Keywords
  • Modeling
  • QBF Programming
  • CNF Encodings

Metrics

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

Abstract

We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.

Cite As Get BibTex

Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine. QBF Programming with the Modeling Language Bule. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.31

Author Details

Jean Christoph Jung
  • Universität Hildesheim, Germany
Valentin Mayer-Eichberger
  • Universität Potsdam, Germany
Abdallah Saffidine
  • University of New South Wales, Sydney, Australia

Supplementary Materials

References

  1. Krzysztof R. Apt, Howard A. Blair, and Adrian Walker. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming, pages 89-148. Morgan Kaufmann, 1988. URL: https://doi.org/10.1016/b978-0-934613-40-8.50006-3.
  2. Fahiem Bacchus. The AIPS '00 planning competition. AI Mag., 22(3):47-56, 2001. URL: https://ojs.aaai.org/index.php/aimagazine/article/view/1571.
  3. Olivier Bailleux and Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. In F. Rossi, editor, 9th International Conference on Principles and Practice of Constraint Programming, volume 2833 of Lecture Notes in Computer Science, pages 108-122. Springer, 2003. Google Scholar
  4. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 31, pages 1177-1221. IOS Press, 2021. Google Scholar
  5. Stefano Bistarelli, Lars Kotthoff, Francesco Santini, and Carlo Taticchi. Summary report for the third international competition on computational models of argumentation. AI Mag., 42(3):70-73, 2021. URL: https://doi.org/10.1609/aimag.v42i3.15109.
  6. Uwe Bubeck and Hans Kleine Büning. Models and quantifier elimination for quantified horn formulas. Discret. Appl. Math., 156(10):1606-1622, 2008. URL: https://doi.org/10.1016/j.dam.2007.10.005.
  7. Tom Bylander. The computational complexity of propositional STRIPS planning. Artif. Intell., 69(1-2):165-204, 1994. URL: https://doi.org/10.1016/0004-3702(94)90081-7.
  8. Michael Cashmore, Maria Fox, and Enrico Giunchiglia. Planning as quantified boolean formula. In ECAI 2012 - 20th European Conference on Artificial Intelligence., volume 242 of Frontiers in Artificial Intelligence and Applications, pages 217-222. IOS Press, 2012. URL: https://doi.org/10.3233/978-1-61499-098-7-217.
  9. Broes De Cat, Bart Bogaerts, Maurice Bruynooghe, Gerda Janssens, and Marc Denecker. Predicate logic as a modeling language: the IDP system. In Declarative Logic Programming: Theory, Systems, and Applications, pages 279-323. ACM / Morgan & Claypool, 2018. URL: https://doi.org/10.1145/3191315.3191321.
  10. Stefano Ceri, Georg Gottlob, and Letizia Tanca. What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng., 1(1):146-166, 1989. URL: https://doi.org/10.1109/69.43410.
  11. Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. ACM Comput. Surv., 33(3):374-425, 2001. URL: https://doi.org/10.1145/502807.502810.
  12. Phan Minh Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell., 77(2):321-358, 1995. URL: https://doi.org/10.1016/0004-3702(94)00041-X.
  13. Paul E. Dunne and Trevor J. M. Bench-Capon. Coherence in finite argument systems. Artif. Intell., 141(1/2):187-203, 2002. URL: https://doi.org/10.1016/S0004-3702(02)00261-8.
  14. Thomas Eiter, Georg Gottlob, and Heikki Mannila. Disjunctive datalog. ACM Trans. Database Syst., 22(3):364-418, 1997. URL: https://doi.org/10.1145/261124.261126.
  15. Jorge Fandinno, François Laferrière, Javier Romero, Torsten Schaub, and Tran Cao Son. Planning with incomplete information in quantified answer set programming. Theory Pract. Log. Program., 21(5):663-679, 2021. URL: https://doi.org/10.1017/S1471068421000259.
  16. Paolo Ferraris and Vladimir Lifschitz. Mathematical foundations of answer set programming. In We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 615-664. College Publications, 2005. Google Scholar
  17. Richard E. Fikes and Nils J. Nilsson. Strips: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2:189-208, 1971. Google Scholar
  18. Martin Gebser, Amelia Harrison, Roland Kaminski, Vladimir Lifschitz, and Torsten Schaub. Abstract gringo. Theory Pract. Log. Program., 15(4-5):449-463, 2015. URL: https://doi.org/10.1017/S1471068415000150.
  19. Martin Gebser, Tomi Janhunen, Roland Kaminski, Torsten Schaub, and Shahab Tasharrofi. Writing declarative specifications for clauses. In 15th European Conference on Logics in Artificial Intelligence JELIA, volume 10021 of Lecture Notes in Computer Science, pages 256-271, 2016. URL: https://doi.org/10.1007/978-3-319-48758-8_17.
  20. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. Google Scholar
  21. E. Giunchiglia, M. Narizzano, L. Pulina, and A. Tacchella. Quantified Boolean Formulas satisfiability library (QBFLIB), 2005. URL: https://www.qbflib.org.
  22. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 428-437, 2018. Google Scholar
  23. Yuliya Lierler and Vladimir Lifschitz. One more decidable class of finitely ground programs. In 25th International Conference on Logic Programming (ICLP), volume 5649 of Lecture Notes in Computer Science, pages 489-493. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02846-5_40.
  24. Valentin Mayer-Eichberger and Abdallah Saffidine. Positional games and QBF: the corrective encoding. In Luca Pulina and Martina Seidl, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 12178 of Lecture Notes in Computer Science, pages 447-463. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_31.
  25. David G. Mitchell and Eugenia Ternovska. A framework for representing and solving NP search problems. In Twentieth National Conference on Artificial Intelligence (AAAI), pages 430-435. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-068.php.
  26. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic with equality. Technical Report MSR-TR-2008-181, Microsoft Research, December 2008. URL: https://www.microsoft.com/en-us/research/publication/deciding-effectively-propositional-logic-with-equality/.
  27. Irfansha Shaik and Jaco van de Pol. Classical planning as QBF without grounding (extended version). CoRR, abs/2106.10138, 2021. URL: http://arxiv.org/abs/2106.10138.
  28. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified boolean formulas. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI, pages 78-84. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  29. Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In 11th International Conference on Principles and Practice of Constraint Programming (CP), pages 827-831, Sitges, Spain, October 2005. Google Scholar
  30. Joost P. Warners. A Linear-Time Transformation of Linear Inequalities into Conjunctive Normal Form. Information Processing Letters, 68(2):63-69, 1998. Google Scholar
  31. Johan Wittocx, Maarten Mariën, and Marc Denecker. Grounding FO and FO(ID) with bounds. J. Artif. Intell. Res., 38:223-269, 2010. URL: https://doi.org/10.1613/jair.2980.
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