qbf2epr: A Tool for Generating EPR Formulas from QBF

Martina Seidl; Florian Lonsing; Armin Biere

qbf2epr: A Tool for Generating EPR Formulas from QBF

Martina Seidl, Florian Lonsing, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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 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.

Original language	English
Title of host publication	Proceedings of PAAR 2012 (Third Workshop on Practical Aspects of Automated Reasoning)
Editors	P. Fontaine, R. Schmidt, S. Schulz
Number of pages	8
Publication status	Published - Jul 2012

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{b6e7341932ae42819fb844a26a8abbad,

title = "qbf2epr: A Tool for Generating EPR Formulas from QBF",

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 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.",

author = "Martina Seidl and Florian Lonsing and Armin Biere",

year = "2012",

month = jul,

language = "English",

editor = "\{P. Fontaine, R. Schmidt, S. Schulz\}",

booktitle = "Proceedings of PAAR 2012 (Third Workshop on Practical Aspects of Automated Reasoning)",

}

TY - GEN

T1 - qbf2epr: A Tool for Generating EPR Formulas from QBF

AU - Seidl, Martina

AU - Lonsing, Florian

AU - Biere, Armin

PY - 2012/7

Y1 - 2012/7

N2 - 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.

AB - 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.

UR - http://www.eprover.org/EVENTS/PAAR-2012/PAAR2012.pdf

M3 - Conference proceedings

BT - Proceedings of PAAR 2012 (Third Workshop on Practical Aspects of Automated Reasoning)

A2 - P. Fontaine, R. Schmidt, S. Schulz, null

ER -

qbf2epr: A Tool for Generating EPR Formulas from QBF

Abstract

Fields of science

JKU Focus areas

Other files and links

Cite this