Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.31
URN: urn:nbn:de:0030-drops-167058
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16705/
Jung, Jean Christoph ; Mayer-Eichberger, Valentin ; Saffidine, Abdallah
QBF Programming with the Modeling Language Bule
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{jung_et_al:LIPIcs.SAT.2022.31,
author = {Jung, Jean Christoph and Mayer-Eichberger, Valentin and Saffidine, Abdallah},
title = {{QBF Programming with the Modeling Language Bule}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {31:1--31:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16705},
URN = {urn:nbn:de:0030-drops-167058},
doi = {10.4230/LIPIcs.SAT.2022.31},
annote = {Keywords: Modeling, QBF Programming, CNF Encodings}
}
| Keywords: | Modeling, QBF Programming, CNF Encodings | |
| Seminar: | 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 28.07.2022 | |
| Supplementary Material: | Software (Source Code): https://github.com/vale1410/bule |
