You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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

Issue title: SAT 2014 Competitions and Evaluations

Article type: Research Article

Authors: Janota, Mikoláša | Jordan, Charlesb | Klieber, Willc | Lonsing, Floriand | Seidl, Martinae | Van Gelder, Allenf

Affiliations: [a] SAT Group, INESC-ID Lisboa, Portugal. E-mail: mikolas.janota@gmail.com | [b] Graduate School of Information Science and Technology, Hokkaido University, Japan. E-mail: skip@ist.hokudai.ac.jp | [c] Software Engineering Institute, Carnegie Mellon University, United States. E-mail: wklieber@cs.cmu.edu | [d] Institute of Information Systems, TU Vienna, Austria. E-mail: florian.lonsing@tuwien.ac.at | [e] Institute for Formal Models and Verification JKU Linz, Austria. E-mail: martina.seidl@jku.at | [f] Jack Baskin School of Engineering, University of California at Santa Cruz, United States. URL: http://www.cse.ucsc.edu/~avg

Keywords: Quantified Boolean formulas, QBF solving, QBF competition

DOI: 10.3233/SAT190108

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 187-206, 2014

Received 1 December 2014
|
Revision received 1 October 2015
|
Published: 1 January 2016
Get PDF open access

Abstract

The QBF Gallery 2014 was a competitive evaluation for QBF solvers organized as part of the FLoC 2014 Olympic Games during the Vienna Summer of Logic. The QBF Gallery 2014 featured three different tracks on formulas in prenex conjunctive normal form (PCNF) including more than 1200 formulas to be solved. Gold, silver, and bronze track medals were awarded to the solvers that solved the most formulas in each of the three tracks. Additionally, the three participants that were most successful over the complete benchmark set were awarded with Kurt Gödel medals, the official prizes of the FLoC 2014 Olympic Games.

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

Show more