QBFGallery 2026

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. The aim of QBFGallery 2026 is to present and evaluate the state of the art in this field.

The QBF Gallery 2026 is part of the FLoC 2026 olympic games.

General Description

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

The goal of the QBFGallery is to empirically assess the state of the art in QBF and DQBF solving 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 2026 Workshop, on July 19th, 2026.

Important Dates (all dates are AoE)

2026-05-17: Submission of benchmarks

2026-05-17: Submissions of solvers

2026-05-20: Feedback on solver submissions

May, June 2026: evaluation runs

2026-07-19: presentation of results at the QBF 2026 Workshop

Tracks

QBFGallery will feature the following tracks:

PCNF track (main track)
Crafted instances track
Random formulas track
2QBF track
Prenex Non-CNF track
DQBF track

Further tracks like a parallel track or a certified track might be organized if there are enough submissions. For suggestions, feel free to contact the organizers.

Submissions

All submissions (solvers and benchmarks) have to be registered via this form.

Solver Submissions

The source code of submitted solvers must be made publicly available with a license that allows research.
It is highly recommended to archive the final submission as an artifact on Zenodo.
Submissions and information in the form can be updated until the deadlines.
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 is the input file. If a solver should be run in different configurations, for each configuration, a script has to be provided.
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.
Submitted systems have to run on a recent Linux 64-bit operating system.

Benchmark Submissions

Benchmark formulas can be submitted in QDIMACS, QCIR, or DQDIMACS format.
The formulas have to be provided under a license that allows their redistribution and modification. In particular, it must be allowed to include formulas selected for the evaluations to be published in a Zenodo artifact and on this webpage.
Also submissions of benchmark generators are welcome. They need to be publicly available and they need to be published under a license that allows research purposes.