论文标题
硬解决方案的硬质量QBF
Hard QBFs for Merge Resolution
论文作者
论文摘要
我们证明了证明系统合并分辨率的第一个真正的QBF证明尺寸的下限（MRES [Olaf Beyersdorff等，2020]），这是Prenex量化布尔公式（QBF）的反驳证明系统。与文献中的大多数QBF分辨率系统不同，MRES中的证明包括分辨率步骤以及有关反向模型的信息，这些信息是句法存储在证明中，作为合并地图。正如[Olaf Beyersdorff等，2020]中所示，这使MRES非常强大：它具有设计策略，并允许对公式的简短证明，这对于经典的QBF分辨率系统很难。 在这里，我们显示了MRE的第一个真正的QBF指数下限，从而发现了MRE的局限性。从技术上讲，结果要么是从电路复杂性（对于限制版本的MRE）转移的，要么是通过组合参数直接获得的（对于完整的MRES）。我们的结果表明，MRES方法在很大程度上与其他QBF分辨率模型（例如QCDCL分辨率系统QRES和QURES以及扩展系统$ \ forall $ exp+res and 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.
