Evaluating QBF Solvers: Quantifier Alternations Matter

Abstract

Competitions of quantified Boolean formula (QBF) solvers are an important driving force for solver development. We consider solvers and benchmarks in prenex conjunctive normal form (PCNF) that participated in the recent QBF competition (QBFEVAL'16) and take a fresh look at the number of solved instances as a measure of solver performance. Rather than ranking solvers by the total number of solved instances, which is common practice in competitions, we determine solver rankings with respect to instances that are solved in classes of instances having a particular number of quantifier alternations. We report experimental results which indicate that solver performance substantially varies depending on the number of alternations in the underlying instance classes. In particular, we observed that solvers implementing orthogonal solving paradigms, such as variable expansion or backtracking search with clause learning, perform better on instances having either few or many alternations, respectively. Consequently, a bias towards instances with a certain number of alternations in a benchmark set may result in a biased solver ranking. In order to avoid biased rankings, our observations motivate the development of alternative performance measures of QBF solvers and competition setups that are more robust with respect to alternations.