H-coloring Dichotomy in Proof Complexity

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\v{s}et\v{r}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.