Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR21-109 | 20th July 2021 10:17

QRAT Polynomially Simulates Merge Resolution.


Authors: Sravanthi Chede, Anil Shukla
Publication: 23rd July 2021 23:10
Downloads: 224


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.

ISSN 1433-8092 | Imprint