2026-07-18T11:53:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16705 2024-03-12T12:00:56Z ddc:004 open_access

QBF Programming with the Modeling Language Bule Jung, Jean Christoph Mayer-Eichberger, Valentin Saffidine, Abdallah Modeling QBF Programming CNF Encodings 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jean Christoph Jung and Valentin Mayer-Eichberger and Abdallah Saffidine 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.31 urn:nbn:de:0030-drops-167058 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.31 eng https://creativecommons.org/licenses/by/4.0/legalcode