The QBF Gallery: Behind the Scenes

TL;DR

This paper discusses the establishment and evaluation of the QBF Gallery, a platform for benchmarking and assessing advances in quantified Boolean formula solving techniques, tools, and benchmarks.

Contribution

It introduces the QBF Gallery as a forum for evaluating QBF solvers and benchmarks, and reports on experiments assessing tool and benchmark quality.

Findings

Assessment of QBF solver performance

Benchmark quality evaluation

Identification of promising research directions

Abstract

Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.