Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.
Seidl, M., Lonsing, F., & Biere, A. (2012). qbf2epr: A Tool for Generating EPR Formulas from QBF. In P. Fontaine, R. Schmidt, & S. Schulz (Eds.), Proceedings of PAAR 2012 (p. 8). http://hdl.handle.net/20.500.12708/54418
E194-03 - Forschungsbereich Business Informatics E192-03 - Forschungsbereich Knowledge Based Systems
-
Published in:
Proceedings of PAAR 2012
-
Date (published):
2012
-
Event name:
Third Workshop on Practical Aspects of Automated Reasoning
-
Event date:
30-Jun-2012 - 1-Jul-2012
-
Event place:
Manchester, EU
-
Number of Pages:
8
-
Peer reviewed:
No
-
Keywords:
QBF; EPR
-
Abstract:
We present the tool qbf2epr which translates quantified Boolean formulas (QBF) to formulas in effectively propositional logic (EPR). The decision problem of QBF is the prototypical problem for PSPACE, whereas EPR is NEXPTIME-complete. Thus QBF is embedded in a formalism, which is potentially more succinct. The motivation for this work is twofold. On the one hand, our tool generates challenging ben...
We present the tool qbf2epr which translates quantified Boolean formulas (QBF) to formulas in effectively propositional logic (EPR). The decision problem of QBF is the prototypical problem for PSPACE, whereas EPR is NEXPTIME-complete. Thus QBF is embedded in a formalism, which is potentially more succinct. The motivation for this work is twofold. On the one hand, our tool generates challenging benchmarks for EPR solvers.
On the other hand, we are interested in how EPR solvers perform compared to QBF solvers and if there are techniques implemented in EPR solvers which would also be valuable in QBF solvers and vice versa. Furthermore, we provide an improved encoding of QBF in EPR based on dependency schemes which are a powerful concept in QBF solving.
en
Project title:
FAME: Formalizing and Managing Evolution in Model-Driven Engineering (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
