QBF Resolution Systems and their Proof Complexities

ABSTRACT. Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof length to its extended variants: long-distance Q-resolution (LQ-resolution) and Q-resolution with resolution over universal literals (QU-resolution). The relative proof power between LQ-resolution and QU-resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further proposes a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ-resolution proofs in contrast to their exponential Q-resolution counterparts.