Experimental analysis of the computational cost of evaluating Quantified Boolean Formulae

Although Knowledge Representation is full of reasoning problems that have been formally proved to be both NP-hard and coNP-hard, the experimental analysis has largely focused on problems belonging to either NP or coNP. We still do not know, for example, whether well studied phenomena such as “phase transition”, which show up for many NP-complete problems (e.g., sat) happen for Σ p 2 -complete problems, and whether they are related to an “easy-hard-easy” pattern or not. The goal of this paper is to show some results of an ongoing experimental analysis that aims to provide reasonable answers to such questions. We analyze the problem of evaluating Quantified Boolean Formulae, which is the prototypical complete problem for all levels of the Polynomial Hierarchy, the computationally simplest hierarchy of complexity classes above NP of great interest to KR.