DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2022.31

QBF Programming with the Modeling Language Bule

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

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2022.31},
  URN =		{urn:nbn:de:0030-drops-167058},
  doi =		{10.4230/LIPIcs.SAT.2022.31},
  annote =	{Keywords: Modeling, QBF Programming, CNF Encodings}
}

Search Results

Documents authored by Mayer-Eichberger, Valentin

QBF Programming with the Modeling Language Bule

Abstract

Cite as

Thanks for your feedback!

Could not send message