QBF Gallery 2014 (Competition)


  • 2014-04-09: deadline for submission of PCNF solvers extended
  • 2014-04-08: announcement of QCIR format for non-prenex, non-CNF formulas
  • 2014-03-24: announcement of judges
  • 2014-02-10: website online

Important Dates

  • 2014-03-05: registration open
  • 2014-04-27: final submission of PCNF solvers
  • 2014-04-30: final submission of Non-PCNF solvers, any tools, and benchmarks
  • April, May, June 2014: evaluation runs
  • July 13 2014: presentation of results at the QBF 2014 Workshop

Event affiliated to


Related Web Pages

SAT 2014

QBF Workshop 2014

QBF Gallery 2013



Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT).

Many problems from application domains such as model checking, formal verification or synthesis are PSPACE-complete, and hence could be encoded in QBF. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not yet widely applied to practical problems in industrial settings.

General Description

The QBF Gallery is an adjunct of the QBF Workshop 2014 that will be held in conjunction with SAT 2014.

The goal of the QBF Gallery is to empirically assess the state-of-the-art in QBF solving as well as collect and select expressive benchmarks. QBF researchers and users are invited to contribute their solvers, tools, and benchmarks to be used for evaluation. Submission of new benchmarks related to QBF applications which have been shown to be hard for QBF solvers in the past are particularly welcome.

The overall exhibition of the results of the QBF Gallery will be staged during the QBF 2014 Workshop, on July 13th, 2014.

The QBF Gallery will be part of the FLoC Olympic Games and will honor the winners in the first award ceremonies.

If available, new benchmarks submitted by participants as well as benchmarks from QBFLIB which have not been used during previous editions of QBFEVAL will be considered for evaluation runs.

Submission Procedure

  1. Register your submission(s) in Easychair by providing a short abstract briefly describing the type of the planned submission (e.g. what kind of solver, application domain of benchmarks,...). Registered participants will be informed by email on any news. The actual submission does not have to be provided until the deadline applying to the kind of contribution. Registration before the submission is not mandatory, but recommended.
  2. Upload your submissions(s). You will receive feedback after a few days if your submission(s) apply to the rules stated below.
Submission Details:
  • Submitted tools will not become publicly available from the organizers (neither to the other participants). Used benchmarks will be published on this webpage.
  • Linux x86 (64 bit) is the standard platform on which all tools are expected to operate.
  • Tools may be submitted as source code or as statically linked binaries. If source code is submitted, self explaining installation instructions have to be provided.
  • Tools may consist of multiple files (binaries as well as bash, python, and perl scripts).
  • Each submitter may have up to three solver submissions (different solvers, different configurations, additional preprocessors, ...) in one solver category.
  • If different configurations of one solver shall participate, a script has to be provided for each configuration.
  • The only argument of a solver shall be the input file.
  • If the solver concludes that the formula is satisfiable, it shall return 10, if the solver concludes that the formula is unsatisfiable, it shall return 20. All other return values will be considered as failure.
  • The input format for CNF benchmarks and tools is QDIMACS.
  • For (non-prenex) non-CNF solvers and benchmarks the QCIR format will be used. This format supports non-prenex non-cnf quantified circuits.
    • Benchmarks may use the full format
    • Solvers may assume the input formulas to be in the syntactically restricted cleansed format (see QCIR format). If you have a solver which supports the full format, please contact the organizers.
    • For prenex non-CNF solvers, the formulas will be provided in prenex normal form.
    • Converter from qpro format to QCIR
    • Converter from QDIMACS to QCIR (by Will Klieber)
  • Submissions have to be uploaded in Easychair as zip, tgz, or gz file.
  • If you provide benchmarks, please submit a description with background information and an external link to the benchmarks. If you don't have webspace where you can put your benchmarks, please write an email to qbfgallery2014@easychair.org.
  • If you submit a benchmark generator, please provide use some options which you consider as interesting.

Types of Submissions

QBF Gallery is open to all kind of submissions related to evaluating and applying QBF including but not limited to:

  • CNF solvers
  • Non-CNF solvers
  • 2QBF solvers
  • Preprocessors
  • Benchmark generators
  • Sets of benchmark formulas
  • Scoring and evaluation methods

Execution and Presentation of Results



Send any requests and questions to qbfgallery2014@easychair.org