Access the full text.
Sign up today, get DeepDyve free for 14 days.
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 Exp+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 Exp+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 (Exp+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 Bning et al.  for the strong expansion-based calculus IR-calc.
ACM Transactions on Computation Theory (TOCT) – Association for Computing Machinery
Published: Sep 12, 2019
Keywords: Proof complexity
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.