论文标题
CSP的证明复杂性
Proof complexity of CSP
论文作者
论文摘要
CSP（约束满意度问题）是一类问题，这些问题决定是否存在实例关系结构到目标结构的同态性。 CSP二分法是Zhuk（2020，J。Acm，67）和Bulatov（2017，Focs，58）最近证明的深刻结果。它确定对于任何固定的目标结构，CSP都是NP组件或$ P $ - 时间可溶剂。 Zhuk的算法在多项式时间内解决了CSP的约束语言，其近乎一致的多态性较弱。 对于$ P $ - 时间CSP的负面实例，探索其证明复杂性是合理的。我们表明，Zhuk算法的健全性可以在有限的算术理论中证明，即在理论中$ v^1 $增强，由三个特殊的通用代数公理增强。这意味着任何模拟扩展分辨率的命题证明系统和证明这三个公理的理论都允许$ p $ size证明所有负面实例的固定$ p $ - 时间-Time CSP的证明。
The CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It establishes that for any fixed target structure, CSP is either NP-complete or $p$-time solvable. Zhuk's algorithm solves CSP in polynomial time for constraint languages having a weak near-unanimity polymorphism. For negative instances of $p$-time CSPs, it is reasonable to explore their proof complexity. We show that the soundness of Zhuk's algorithm can be proved in a theory of bounded arithmetic, namely in the theory $V^1$ augmented by three special universal algebra axioms. This implies that any propositional proof system that simulates both Extended Resolution and a theory that proves the three axioms admits $p$-size proofs of all negative instances of a fixed $p$-time CSP.
