The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games

Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, Allen Van Gelder


The QBFGallery 2014 was a competitive evaluation for QBF solvers organized in the context of the FLoC 2014 Olympic Games of the Vienna Summer of Logic. Quantified Boolean formulas (QBF) extend formulas of propositional logic by existential and universal quantifiers over the propositional variables and, thus, lift the satisfiablity problem from NP to PSPACE. In consequence, there are many application problems from fields like verification, synthesis, and planning that can be encoded efficiently in QBF. This  motivates the quest for efficient QBF solvers.

The QBFGallery 2014 invited the developers of QBF solvers to submit their tools to a competitive evaluation in a uniform environment. Gold, silver, and bronze track medals were awarded to the solvers that solved the most formulas in each of three different tracks covering various kinds of benchmarks. Additionally, the three participants that were most successful overall were decorated with Kurt G ̈odel medals, the official prizes of the  Olympic Games.

In this paper, we give an overview of the setup of the competition, we briefly review the participating solvers, and finally report on the results of the QBFGallery 2014.

Full Text:



  • There are currently no refbacks.