证明复杂性中的H-染色二分法
H-coloring Dichotomy in Proof Complexity
摘要：
无向单图的$\mathcal{H}$ -染色问题是一类约束满足问题（CSP）中的计算问题：图$\mathcal{G}$的$\mathcal{H}$ -染色是从$\mathcal{G}$到$\mathcal{H}$的同态，问题是在给定$\mathcal{G}$的情况下，判定固定的$\mathcal{H}$是否存在同态. $\mathcal{H}$ -着色问题的二分法定理由Hell和Nešetzil在1990年证明（Zhuk和Bulatov最近证明了所有CSP的类似定理），它说对于每个$\mathcal{H}$，问题要么是$p$ -时间可判定的，要么是$NP$ -完全的。由于CSP的不可满足实例的否定可以表示为命题重言式，因此研究CSP的证明复杂性似乎是很自然的。我们表明，在$p$时间的情况下的$\mathcal{H}$着色问题的决策算法可以在一个相对较弱的理论和重言式表达的负面情况下，这样的$\mathcal{H}$有简短的证明命题证明系统$R^*(log)$，一个温和的扩展决议。事实上，当公式表示为不可满足的子句集时，它们具有$p$大小的分辨率证明。为了建立这一点，我们使用一个众所周知的有界算术理论和命题证明系统之间的联系。我们补充这一结果的下界结果，持有许多弱证明系统的一个特殊的例子$NP$ -完整的情况下的$\mathcal{H}$着色问题，使用已知的结果证明复杂性的鸽子洞原则。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
