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

[  overview | workflow | format | certified | download | license ]

QBFcert

Overview

QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF). QBFcert supports QRP format for resolution-based traces and proofs. The corresponding QBF certificate is represented in AIGER format.

QBFcert is QBF- and SAT-solver independent, i.e., it is possible to plug any QBF resp. SAT solver into the framework as long as the QBF solver is able to produce resolution-based traces or proofs in binary or ascii QRP format.

Workflow

QBFcert Workflow

Input/Output Format

QBFcert supports ascii and binary QRP format for resolution-based traces and proofs. The corresponding QBF certificate is represented as a set of And-Inverter-Graphs (AIGs) in either ascii or binary AIGER format.
Note that CertCheck generates a propositional formula in DIMACS format.

Certified Instances

Here is a list of instances that were certified with QBFcert (with QRPcheck v1.0.3, QRPcert v1.0.1, CertCheck v1.0.1) within a time limit of 1800 seconds and a memory limit of 7 GB:

Download

This package contains a QBF solver (DepQBF), QRPcheck, QRPcert, CertCheck, and a SAT solver (Lingeling).
See the README file for instructions and release notes, which is also part of the distribution.

Source Code (individual tools)

  • QRPcheck, a proof checker for resolution proofs of (un)satisfiability in binary/ascii QRP format.
  • QRPcert, a tool for extracting QBF certificates from resolution proofs in binary/ascii QRP format.
  • CertCheck, a tool for merging a QBF certificate with its input formula to be validated by a SAT solver.
  • You might also want to use:
    • DepQBF, a search-based QBF solver that supports tracing in binary/ascii QRP format.
    • Lingeling, a state-of-the-art SAT solver.

License

QBFcert is maintained by Aina Niemetz and Mathias Preiner.
All tools included are released under the GNU GPLv3 License (see the resp. tool pages for further information).