Tags:Library of encodings, Modeling and QBF Programming
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 might be existentially or universally quantified. The language features a natural minimal models semantics and a subsequent grounding based generation of a quantified Boolean formula in conjunctive normal form. This makes Bule easy and intuitive to learn and an ideal language to get started with modeling of PSPACE problems in terms of QBF. We implemented a tool of the same name that 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 showcase its use on several examples.