计数解析：线性映射布尔立方体补集的成员证明的下界
摘要：一个新的方法用于证明Res(lin$\_{\mathbb{F}_p}$)证明系统中dag-like证明的下界。这里$\mathbb{F}_p$是一个素数阶$p \geq 5$的有限域。在之前的研究中，已经证明了Res(lin$\_{\mathbb{F}}$)证明系统中任意dag-like证明的指数级下界，前提是$\mathbb{F}$是特征为0且不是CNF的一个实例。对于二进制数值原理$x_1 + 2x_2 + \dots + 2^{n-1}x_n = -1$，该下界的证明实质上使用了特征为0的特殊性质，对于有限域和CNF的证明下界没有给出线索。本研究旨在构建二进制数值原理和CNF证明下界之间的桥梁，我们开始开发一种方法，用于证明线性映射$A$的形式为$b \notin A(\{0,1\}^n)$的tautologies的dag-like Res(lin$\_{\mathbb{F}_p}$)证明下界。这种tautology的否定可以用Res(lin$\_{\mathbb{F}_p}$)的语言表示为一个在布尔赋值上不可满足的线性方程组$A \cdot x = b$。这种形式的实例在某种程度上比CNF简单，这使得对其Res(lin$\_{\mathbb{F}_p}$)证明的分析更易接近，并可能受益于线性代数和加性组合数学工具的帮助。我们利用纠错码的概念和我们引入的$(s, r)$-强韧性这一线性系统$A \cdot x = b$的组合代数性质，识别了形式为$A \cdot x = b$的实例的难度准则。我们证明了Res(lin$\_{\mathbb{F}_p}$)的两个片段的下界，这两个下界捕捉了Res(lin$\_{\mathbb{F}_p}$)证明的两个互补的方面，并构成了一种用于处理一般dag-like Res(lin$\_{\mathbb{F}_p}$)证明的组合工具箱。
作者：Fedor Part
论文ID：2202.08214
分类：Computational Complexity
分类简称：cs.CC
提交时间：2022-02-17