Since the introduction of the Ideal Proof System (IPS) by Grochow and Pitassi (J. ACM 2018), a substantial body of work has established size lower bounds for IPS and its fragments. In particular, Forbes, Shpilka, Tzameret, and Wigderson (Theory Comput. 2021) developed the main lower-bound frameworks for restricted IPS fragments, namely functional lower bounds and the hard multiples method, while Alekseev, Grigoriev, Hirsch, and Tzameret (SIAM J. Comput. 2024) gave a general template for conditional lower bounds for full IPS. Yet all these lower bounds apply only to purely algebraic formulas over a field, that is, non-Boolean formulas not directly expressible in propositional logic. Proving lower bounds for CNF formulas has therefore remained a central open problem in this line of work. The current work resolves this question for IPS over read-once oblivious algebraic branching programs (roABPs) by proving lower bounds for refutations of CNF formulas in this system. Our approach is a rank-based feasible interpolation argument, following the method of Pudlák and Sgall (Proof Complexity and Feasible Arithmetic 1996) for monotone span programs, in which decomposing a given roABP refutation along a variable partition yields a low-dimensional space of polynomials from which we construct a span-program interpolant. We extend their result from Nullstellensatz refutations measured by degree to Nullstellensatz refutations measured by roABP size (i.e., roABP-IPS$_\text{LIN}$).

翻译：自Grochow和Pitassi（J. ACM 2018）引入理想证明系统（IPS）以来，大量工作建立了IPS及其片段的大小下界。特别是Forbes、Shpilka、Tzameret和Wigderson（Theory Comput. 2021）为受限IPS片段发展了主要的下界框架，即函数下界与硬倍数方法，而Alekseev、Grigoriev、Hirsch和Tzameret（SIAM J. Comput. 2024）为完整IPS的条件性下界提供了通用模板。然而，所有下界仅适用于域上的纯代数公式，即不能直接以命题逻辑表达的布尔公式。因此，证明CNF公式的下界始终是该方向的核心开放问题。本文针对只读一次无歧义代数分支程序（roABP）上的IPS解决了该问题，证明了此系统中CNF公式反驳的下界。我们的方法是一种基于秩的可行插值论证，遵循Pudlák和Sgall（Proof Complexity and Feasible Arithmetic 1996）用于单调分支程序的思路：沿变量划分分解给定的roABP反驳，得到一个低维多项式空间，并由此构造一个分支程序插值器。我们将他们的结果从以度数衡量的Nullstellensatz反驳扩展至以roABP规模（即roABP-IPS$_\text{LIN}$）衡量的Nullstellensatz反驳。