线性方程组的对称性求解
Resolution with Symmetry Rule applied to Linear Equations
摘要：
本文考虑了使用克里希那穆尔西的经典对称性规则时，解决证明的长度。我们表明，不一致的线性方程系统的有界宽度在一个固定的有限域$\mathbb{F}_p$与$p$一个素数，在他们的标准编码CNFs，多项式长度分辨率时，使用局部对称规则（SRC-II）。因此，它遵循的多足类的情况下，图同构问题编码为CNF公式有多项式长度的解决证明。这与这些图上的个性化细化算法的指数下限形成对比。对于Cai-Fürer-Immerman图，Torán证明了其分辨率证明的指数下界（SAT 2013），我们还证明了全局对称规则（SRC-I）已经足以允许多项式长度证明。
英文摘要：
This paper considers the length of resolution proofs when using Krishnamurthy's classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fixed finite field $\mathbb{F}_p$ with $p$ a prime have, in their standard encoding as CNFs, polynomial length resolutions when using the local symmetry rule (SRC-II). As a consequence it follows that the multipede instances for the graph isomorphism problem encoded as CNF formula have polynomial length resolution proofs. This contrasts exponential lower bounds for individualization-refinement algorithms on these graphs. For the Cai-Fürer-Immerman graphs, for which Torán showed exponential lower bounds for resolution proofs (SAT 2013), we also show that already the global symmetry rule (SRC-I) suffices to allow for polynomial length proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
