Twelve Years of QBF Evaluations: QSAT Is PSPACE-Hard and It Shows
Issue title: Special issue of the 22nd RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion”
Guest editors: Stefano Bistarelli, Andrea Formisano, Marco Maratea and Paolo Torroni
Affiliations: [a] Lehrstuhl für Rechnerarchitektur Georges-Köhler-Allee 051 79110 Freiburg i.B., Germany [email protected] | [b] DIBRIS, Università degli Studi di Genova Via Opera Pia 13, 16145 Genova, Italy [email protected] | [c] POLCOMING, Università degli Studi di Sassari Viale Mancini 5, 07100 Sassari, Italy [email protected] | [d] DIBRIS, Università degli Studi di Genova Via Opera Pia 13, 16145 Genova, Italy [email protected] | [e] DIBRIS, Università degli Studi di Genova Via Opera Pia 13, 16145 Genova, Italy [email protected]
Correspondence:
[*]
Address for correspondence: POLCOMING Department, Universit`a di Sassari, Viale Mancini n. 5 – 07100 Sassari – Italy
Abstract: Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.
