论文标题
H-彩色二分法在证明复杂性方面
H-coloring Dichotomy in Proof Complexity
论文作者
论文摘要
$ \ Mathcal {h} $ - 无向简单图的着色问题是来自一系列约束满意度问题（CSP）的一个计算问题：$ \ Mathcal {h} $ - 图形$ \ Mathcal {g g} $的颜色是$ \ nathcal to proginal copsign $ \ nathcal to $ ression coply cops $ { $ \ MATHCAL {H} $，给定$ \ Mathcal {G} $，如果是否存在同构。 $ \ Mathcal {h} $ - 着色问题的二分法定理证明了1990年的Nešetêil（Zhuk和Bulatov最近证明了所有CSP的类似定理），它说，对于每个$ \ Mathcal {h} $，问题是$ p $ p $ - $ p $ - $ $ np $ np，由于对CSP不满意实例的否定可以表示为命题重言式，因此研究CSP的证明复杂性似乎很自然。 We show that the decision algorithm in the $p$-time case of the $\mathcal{H}$-coloring problem can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such $\mathcal{H}$ have short proofs in propositional proof system $R^*(log)$, a mild extension of resolution.实际上，当公式表示为不满意的条款集时，它们具有$ p $ size的分辨率证明。为了建立这一点，我们使用有界算术和命题证明系统理论之间的众所周知的联系。我们通过$ \ Mathcal {H} $ - 着色问题的特殊示例的许多弱验证系统的下限结果来补充该结果，该示例使用了有关PigeOnhole原理的证明复杂性的已知结果。
The $\mathcal{H}$-coloring problem for undirected simple graphs is a computational problem from a huge class of the constraint satisfaction problems (CSP): an $\mathcal{H}$-coloring of a graph $\mathcal{G}$ is just a homomorphism from $\mathcal{G}$ to $\mathcal{H}$ and the problem is to decide for fixed $\mathcal{H}$, given $\mathcal{G}$, if a homomorphism exists or not. The dichotomy theorem for the $\mathcal{H}$-coloring problem was proved by Hell and Nešetřil in 1990 (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each $\mathcal{H}$ the problem is either $p$-time decidable or $NP$-complete. Since negations of unsatisfiable instances of CSP can be expressed as propositional tautologies, it seems to be natural to investigate the proof complexity of CSP. We show that the decision algorithm in the $p$-time case of the $\mathcal{H}$-coloring problem can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such $\mathcal{H}$ have short proofs in propositional proof system $R^*(log)$, a mild extension of resolution. In fact, when the formulas are expressed as unsatisfiable sets of clauses they have $p$-size resolution proofs. To establish this we use a well-known connection between theories of bounded arithmetic and propositional proof systems. We complement this result by a lower bound result that holds for many weak proof systems for a special example of $NP$-complete case of the $\mathcal{H}$-coloring problem, using the known results about proof complexity of the Pigeonhole Principle.
