Quantified Boolean formulas (QBF) and Dependency Quantified Boolean formulas (DQBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. Many problems from application domains such as model checking, formal verification, synthesis and AI can be efficiently encoded in QBF or DQBF. Considerable progress has been made in (D) QBF solving throughout the past years. The aim of QBFGallery 2023 is to present and evaluate the state of the art as a joint community effort.

General Description

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

The goal of the QBFGallery is to empirically assess the state of the art in QBF and DQBF olving as well as collect and select expressive benchmarks. (D)QBF researchers and users are invited to contribute their solvers, tools, and benchmarks to be used for evaluation or participate in the organization of the evaluation.

Submission of new benchmarks related to (D)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 QBFGallery will be staged during the QBF 2023 Workshop, on July 4th, 2023.

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.

Results

The results are summarized in the presentation given at SAT 2023.

Benchmarks

The formula sets used for the PNCNF-track and the PCNF-track.

Participation

Write an email to qbfgallery2023-admin if you want

  • to participate in the organization of QBFGallery23 or

  • to submit a tool or benchmarks or

  • both

Submission

  • Submitted tools will not become publicly available from the organizers (neither to the other participants).

  • Used benchmarks will be published (most likely on this website).

  • 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 true, it shall return 10, if the solver concludes that the formula is false, it shall return 20. All other return values will be considered as failure.

  • If you provide benchmarks, please submit a description with background information and an external link to the benchmarks.

  • If you submit a benchmark generator, please provide use some options which you consider as interesting.

Types of Submissions

QBFGallery is open to all kind of submissions related to evaluating and applying QBF/DQBF 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

  • The QBFGallery will be run at the StarExec cluster and/or a compute cluster at JKU Linz.

  • The runs will be done during May and June 2023.

  • The results will be announced at the QBF Workshop 2023 and the SAT Conference 2023.

Important Dates

2023-03-31: intention to submit or contribute in the organization

2023-04-30: final submission of tools and benchmarks

May, June 2023: evaluation runs

2023-07-04: presentation of results at the QBF 2023 Workshop

Organizers

  • Luca Pulina

  • Martina Seidl

  • Simone Heisinger

Contact

Send any requests and questions to Martina Seidl.