Antichain-Based QBF Solving

摘要

We consider the problem of QBF solving viewed as a reachability problem in an exponential And-Or graph. Antichain-based algorithms for reachability analysis in large graphs exploit certain subsumption relations to leverage the inherent structure of the explored graph in order to reduce the effect of state explosion, with high performance in practice. In this paper, we propose simple notions of subsumption induced by the structural properties of the And-Or graphs for QBF solving. Subsumption is used to reduce the size of the search tree, and to define compact representations of certificates (in the form of antichains) both for positive and negative instances of QBF. We show that efficient exploration of the reduced search tree essentially relies on solving variants of Max-SAT and Min-SAT. Preliminary stand-alone experiments of this algorithm show that the antichain-based approach is promising.