New Resolution-Based QBF Calculi and Their Proof Complexity

摘要

Modern QBF solvers typically use two different paradigms, conflict-driven clause learning (CDCL) solving or expansion solving. Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of these solvers, with Q-Resolution and its extensions relating to CDCL solving and VExp+Res relating to expansion solving. This article defines two novel calculi, which are resolution-based and enable unification of some of the principal existing resolution-based QBF calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based calculus VExp+Res. However, the proof complexity of the QBF resolution proof systems is currently not well understood. In this article, we completely determine the relative power of the main QBF resolution systems, settling in particular the relationship between the two different types of resolution-based QBF calculi; proof systems for CDCL-based solvers (Q-resolution, universal, and long-distance Q-resolution) and proof systems for expansion-based solvers (VExp+Res and its generalizations IR-calc and IRM-calc defined here). The most challenging part of this comparison is to exhibit hard formulas that underlie the exponential separations of the aforementioned proof systems. To this end, we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths-of-proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems such as long-distance Q-resolution and extensions. With a completely different and novel counting argument, we show the hardness of the prominent formulas of Kleine Biining et al. [51] for the strong expansion-based calculus IR-calc.