Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hard QBFs for Merge Resolution

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood

TL;DR

This work proves the first genuine quantified Boolean formula (QBF) proof size lower bounds for the proof system Merge Resolution, a refutational proof system for prenex QBFs with a CNF matrix, thereby uncovering limitations of MRes.

Abstract

We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first genuine QBF exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems $\forall$Exp+Res and IR.

Hard QBFs for Merge Resolution

TL;DR

This work proves the first genuine quantified Boolean formula (QBF) proof size lower bounds for the proof system Merge Resolution, a refutational proof system for prenex QBFs with a CNF matrix, thereby uncovering limitations of MRes.

Abstract

We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first genuine QBF exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems Exp+Res and IR.

Paper Structure

This paper contains 16 sections, 22 theorems, 4 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Organization of this paper
  3. Preliminaries
  4. Quantified Boolean formulas
  5. The Merge Resolution proof system
  6. Lower bounds
  7. Lower bounds for generic formulas
  8. The QParity formulas
  9. The LQParity formulas
  10. The Completion Principle formulas
  11. Lower bound for tree-like $\text{MRes}$
  12. Lower bound for regular $\text{MRes}$
  13. The KBKF-lq formulas
  14. Relations among proof systems
  15. Conclusions and Future Work
  16. ...and 1 more sections

Key Result

lemma 1

Let $\Phi=Q\cdot\phi$ be a QBF with existential variables $X$ and universal variables $U$. Let $\Pi \stackrel{\mathsmaller{\mathsf{def}}}{=} L_1, \ldots, L_m$ be an $\text{MRes}$ refutation of $\Phi$, where each $L_i = (C_i , \{M_i^u \mid u \in U \})$. Further, for each $i \in [m]$, Then for each $\alpha \in A_i$, the (partial) assignment $(\alpha, h_i(\alpha))$ falsifies at least one clause of $

Figures (1)

  • Figure 1: Visual summary of the proof complexity landscape, with new results shown in bold. Lines from/to a big grey box mean that the line is from/to every proof system within the box. New separations are summarised in \ref{['cor:tree-and-regular-MRes-incomparable-with-five-systems', 'cor:MRes-incomparable']}.

Theorems & Definitions (32)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • lemma 1: Extracted/adapted from DBLP:journals/jar/BeyersdorffBM21 Section 4.3, (Proof of Lemma 21)
  • proposition 1: DBLP:journals/jar/BeyersdorffBM21
  • Theorem 3.1
  • definition 7
  • ...and 22 more