适用于Merge Resolution的难QBF问题
Hard QBFs for Merge Resolution
AI总结：
该研究首次证明了QBF证明系统MRes的指数级证明规模下界，揭示其局限性，同时表明MRes与其他主流QBF归结模型在方法上基本正交。
摘要：
我们首次证明了证明系统Merge Resolution（MRes，出自Olaf Beyersdorff等人2020年的研究）的真正QBF证明规模下界，MRes是一种用于求解带CNF矩阵的前束量化布尔公式（QBF）的反驳式证明系统。与文献中大多数QBF归结系统不同，MRes的证明由归结步骤以及反模型信息组成，反模型以合并映射的形式语法化地存储在证明中。正如Olaf Beyersdorff等人2020年的研究所示，这一特性让MRes具备强大能力：它通过设计实现了策略提取，并且能为经典QBF归结系统难以处理的公式生成短证明。\n 本文中我们给出了MRes的首个真正QBF指数级下界，由此揭示了MRes的局限性。从技术层面看，这些结果要么从电路复杂度的界推导而来（针对MRes的受限版本），要么通过组合论证直接得到（针对完整MRes）。我们的结果表明，MRes方法与其他QBF归结模型（如QCDCL归结系统QRes、QURes，以及扩展系统∀Exp+Res和IR）在很大程度上是正交的。
英文摘要：
We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first genuine QBF exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems $\forall$Exp+Res and IR.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
