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

Report of the Third QBF Solvers Evaluation1

Issue title: SAT 2005 Competitions and Evaluations

Guest editors: Daniel Le Berre and Laurent Simon

Article type: Research Article

Authors: Narizzano, Massimo | Pulina, Luca | Tacchella, Armando

Affiliations: Laboratory of Systems and Technologies for Automated Rasoning (STAR-Lab), DIST, University of Genoa, Viale Causa, 13 – 16145 Genoa, Italy. E-mails: mox@dist.unige.it, luca@star.dist.unige.it, tac@dist.unige.it

Note: [1] The authors would like to thank the anonymous reviewers for their help in improving the quality of this manuscript, and all the participants to the QBF evaluation for submitting QBF instances and solvers. The work of the authors is partially supported by grants from MIUR and by a grant from Intel Corporation.

Keywords: quantified Boolean formulas, empirical evaluation, automated reasoning tools

DOI: 10.3233/SAT190019

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 145-164, 2006

Received 1 October 2005
|
Revision received 1 February 2006
|
Published: 1 March 2006
Get PDF open access

Abstract

This paper reports about the 2005 comparative evaluation of solvers for quantified Boolean formulas (QBFs), the third in a series of non-competitive events established with the aim of assessing the advancements in the field of QBF reasoning and related research. We evaluated thirteen solvers on a test set of more than three thousands QBFs, selected from instances submitted to the evaluation and from those available at http://www.qbflib.org. In the paper we present the evaluation infrastructure, from the criteria used to assemble the test set to the hardware set up, and we show different views about the results obtained, highlighting the strength of different solvers and the relative hardness of the instances included in the test set.

Show more