Algorithmic Aspects of Todas Theorem

Abstract

Toda's Theorem is a fundamental result in computational complexity theory, whose proof is based on a reduction from a QBF problem with a constant number of quantifiers to a model counting problem. The recent progress in model counting tools raises the question of whether this reduction, henceforth called Toda's reduction, can be utilized to construct a practical QBF solver. This question follows a line of research that revisits theoretical results from an algorithmic aspect, and thus brings new theoretical and engineering challenges. For Toda's reduction these challenges arise mainly because the reduction is purely theoretical and based on ideas that are entirely orthogonal to the search-space approach used by current QBF solvers. In this work, we address this question by transforming Toda's reduction into a concrete probabilistic QBF solver that uses model counting as an oracle. A naive implementation is hopeless due to a massive formula blow-up. Therefore we next analyze and identify three main factors that drive the blow-up. While we present solutions that overcome some of the factors, we also discuss the limitations of some, and show that one of the factors, the union bound factor, largely overlooked in the literature, is in fact dominant and in some cases unavoidable. We then show how, for some cases, even this factor can be avoided, and report our preliminary results on a prototype implementation.