QRAT Polynomially Simulates Merge Resolution

TL;DR

This paper proves that the QRAT proof system can polynomially simulate Merge Resolution (MRes), demonstrating QRAT's greater proof complexity power and providing the first known simulation result for MRes.

Contribution

It establishes that QRAT strictly p-simulates MRes, the first such simulation result, highlighting QRAT's enhanced proof capabilities over MRes.

Findings

QRAT can polynomially simulate MRes.

SquaredEquality formulas have short QRAT refutations.

First known simulation result for MRes.

Abstract

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The QRAT [Heule et al. J. Autom. Reason.'2017] proof system was designed to capture QBF preprocessing. QRAT can simulate both the expansion-based proof system $\forall$Exp+Res and CDCL-based QBF proof system LD-Q-Res. A family of false QBFs called SquaredEquality formulas were introduced in [Beyersdorff et al. J. Autom. Reason.'2021] and shown to be easy for MRes but need exponential size proofs in Q-Res, QU-Res, CP+$\forall$red, $\forall$Exp+Res, IR-calc and reductionless LD-Q-Res. As a result none of these systems can simulate MRes. In this paper, we show a short QRAT refutation of the SquaredEquality formulas. We further show that QRAT strictly p-simulates MRes. Besides highlighting the power of QRAT system, this work also presents the first simulation result for MRes.