Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

QBF Merge Resolution is powerful but unnatural

Meena Mahajan, Gaurav Sood

TL;DR

It is shown that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU-Res and IRM, the most powerful among currently known resolution-based QBF proof systems, and that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening.

Abstract

The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU$^+$-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU$^+$-Res. Our proof method reveals two additional and curious features about M-Res: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over M-Res without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege $+$ $\forall$red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).

QBF Merge Resolution is powerful but unnatural

TL;DR

It is shown that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU-Res and IRM, the most powerful among currently known resolution-based QBF proof systems, and that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening.

Abstract

The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU-Res. Our proof method reveals two additional and curious features about M-Res: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over M-Res without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).
Paper Structure (14 sections, 24 theorems, 10 equations, 1 figure)

This paper contains 14 sections, 24 theorems, 10 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Quantified Boolean Formulas
  4. Proof systems
  5. The Merge Resolution proof system
  6. Power of Merge Resolution
  7. Advantage over IRM
  8. Advantage over LQU+Res
  9. Role of weakenings, and unnaturalness
  10. Weakenings
  11. Simulation by eFrege with universal reduction
  12. Unnaturalness
  13. Conclusion and future work
  14. Complete proof of \ref{['lem:kbkflq-mreswu-hard']}

Key Result

Lemma 3.5

$\text{KBKF-lq-weak}$ has polynomial-size $\text{M-Res}$ refutations.

Figures (1)

  • Figure 1: Relations among resolution-based QBF proof systems, with new results and observations highlighted using thicker lines. In addition, regular $\text{$\text{M-ResW}_\forall$}$ strictly p-simulates regular $\text{M-Res}$. Lines from a big grey box mean that the line is from every proof system within the box.

Theorems & Definitions (71)

  • Definition 2.1: CR-JSL79
  • Definition 2.2
  • Definition 2.3
  • Remark 2.4
  • Definition 2.5: BKS-JAIR04
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 61 more