JKU

TNF / INF

team
contact
software
publications
teaching
jobs


GI-Dissertation Award 2020

FMCAD'20 Student Forum Best Student Contribution

SAT'20 Best Presentation Award

GCAI'19 Post and Interaction Award

IJCAI-JAIR 2019 Award

SAT'19 Best Student Paper

CAV'18 Award

HVC'17 Best Paper

ETAPS'17 Test of Time Award

HVC'15 Award

FMCAD'17 Best Paper

CADE'17 Best Paper

BMC

Handbook of Satisfiability

UML@Classroom

UML@Classroom

www.digitaltechnik.org

QBF2EPR

News

  • 2012-06-01: Source code of qbf2epr released.
  • 2012-07-23: option with standard dependency scheme is available.

Overview

qbf2epr is tool which takes a QBF in QDIMACS format as input and produces an EPR formula in TPTP format as output.

Downloads

  • qbf2epr. See also the README file that is part of the package.

Evaluation Results

  • Benchmarks used for experiments are available from QBFEVAL'10 website (260 MB).
  • Log files of DepQBF v0.1 and iprover v0.8.1.
  • Log files of Vampire 0.6.
  • Log files of iprover v0.8.1 where the encoding considers dependencies.
  • Instances which were solved by iProver but not by DepQBF: List
  • Instances which were solved by iProver but not by Quantor: List
  • results of iprover on encoding with and without dependencies

Additional Information

The encoding and some experiments have been published in our paper for the PAAR workshop.

Acknowledgements and License

  • A first version of the tool was developed by Robert Aistleitner and Gregor Dorfbauer and is maintained by Martina Seidl.
  • This version of the source code of qbf2epr is released under an MIT style license.