发表机构
Category Labs（Category Labs）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文首次证明n位乘法结合性的一般归结证明规模为2^{Ω((n/log n)^{1/4})}，通过从完美匹配原理归约，解决Beame和Liew的开放问题，并推广到有界深度Frege系统。
AI 中文摘要
SAT求解器在处理乘法推理时经验上表现不佳，但十多年来我们一直缺乏对这一现象的理论解释。CDCL SAT求解器隐式地搜索归结证明，而此前没有证明规模的下界排除存在求解器未能找到的短证明的可能性。我们首次给出此类下界，证明$n$位乘法结合性的一般归结证明需要规模$2^{\Omega((n/\log n)^{1/4})}$。该下界适用于基于部分乘积求和的一大类乘法器编码，包括SMT求解器中用于位爆破乘法的标准阵列和Wallace树乘法器。这一结果解决了Beame和Liew提出的一个开放问题。证明构造了从有界度二分扩展图上的完美匹配原理到乘法器结合性的归约。Itsykson、Slabodkin和Sokolov证明了该原理对归结是困难的，乘法器结合性的下界由此得出。同样的归约，结合Håstad最近关于奇数网格完美匹配原理的下界，在更强的有界深度Frege证明系统中产生了乘法器结合性的指数下界。
英文摘要
SAT solvers are empirically known to perform poorly when reasoning about multiplication. Yet for over a decade we have lacked a theoretical explanation for this phenomenon. CDCL SAT solvers implicitly search for resolution proofs, and no lower bound on proof size has ruled out the existence of short proofs that solvers simply fail to find. We give the first lower bound of this kind by showing that general resolution proofs of the associativity of $n$-bit multiplication require size $2^{Ω((n/\log n)^{1/4})}$. This lower bound holds for a broad class of multiplier encodings based on partial product summation, including the standard array and Wallace-tree multipliers used to bit-blast multiplication in SMT solvers. This result resolves an open problem of Beame and Liew. The proof constructs a reduction from a perfect-matching principle on bounded-degree bipartite expander graphs to multiplier associativity. Itsykson, Slabodkin, and Sokolov proved that this principle is hard for resolution. The lower bound for multiplier associativity follows. The same reduction, when combined with Håstad's recent lower bound for the perfect-matching principle of the odd grid, yields an exponential lower bound for multiplier associativity in the stronger bounded-depth Frege proof systems.
Comments33 pages, 10 figures. Lean 4 formalization of the main theorems at https://github.com/dysfunctor/associativity
