QRAT多项式模拟合并解析
QRAT Polynomially Simulates Merge Resolution
摘要：
合并分辨率（MRes [Beyersdorff等人，J. Autom.原因的'2021]）是一个量化布尔公式（QBF）的反驳证明系统。每一行MRes都由只有存在字面量的子句组成，以及作为合并映射存储的反模型信息。因此，MRes通过设计进行策略提取。QRAT [Heule等人，J. Autom.原因的'2017]证明系统被设计用于捕获QBF预处理。QRAT可以模拟基于扩展的证明系统$\forall$ Exp+Res和基于CDCL的QBF证明系统LD-Q-Res。原因的'2021]，并且被示出对于MRes是容易的，但是需要在Q-Res、QU-Res、CP+ $\forall$ red、$\forall$ Exp+Res、IR-calc和无归约LD-Q-Res中的指数大小证明。在本文中，我们展示了一个简短的QRAT反驳平方等式公式。我们进一步表明，QRAT严格p-模拟MRes。除了强调QRAT系统的功率，这项工作还提出了第一个模拟结果的MRes。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
