基于线性方程的归结与多线性证明

我们开发并研究了不同强度的命题证明系统的复杂性，这些系统通过允许对线性方程的析取式（而非子句）进行操作来扩展归结法。我们在这些证明系统中展示了针对鸽巢原理、Tseitin 图重言式和团着色重言式等困难重言式的多项式规模驳斥。利用通信博弈技术的（单调）插值法，我们确立了在基于线性方程的归结的某个相当强的片段中驳斥的指数规模下界，以及该片段中（非单调）插值的一般多项式上界。随后，我们应用这些结果扩展并改进了关于多线性证明（在特征为 0 的域上）的先前结果，如 [RazTzameret06] 中所研究。具体而言，我们证明了：1. 使用深度为 3 的多线性公式进行的证明可以多项式模拟基于线性方程的归结的某个相当强的片段。2. 使用深度为 3 的多线性公式进行的证明允许对鸽巢原理和 Tseitin 图重言式进行多项式规模的驳斥。前者改进了先前的结果，该结果仅针对*功能性*鸽巢原理建立了小型多线性证明。后者不同于先前的证明，并适用于任何特征为 0 的域上针对 Tseitin mod p 图重言式的多线性证明。最后，我们将基于线性方程的归结与切割平面证明系统的扩展联系起来。