English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is arefutational proof system for quantified Boolean formulas (QBF). Each line ofMRes consists of clauses with only existential literals, together withinformation of countermodels stored as merge maps. As a result, MRes hasstrategy extraction by design. The QRAT [Heule et al. J. Autom. Reason.'2017]proof system was designed to capture QBF preprocessing. QRAT can simulate boththe expansion-based proof system $\forall$Exp+Res and CDCL-based QBF proofsystem 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 butneed 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 thesesystems can simulate MRes. In this paper, we show a short QRAT refutation ofthe SquaredEquality formulas. We further show that QRAT strictly p-simulatesMRes. Besides highlighting the power of QRAT system, this work also presentsthe first simulation result for MRes.

QRAT Polynomially Simulates Merge Resolution