Logic seminar

H-Coloring Dichotomy in Proof Complexity

The H-Coloring problem can be considered as an example of the computational problem from a huge class of constraint satisfaction problems (CSP): an H-Coloring of a graph G is just a homomorphism from G to H. The dichotomy theorem for H-Coloring was proved by Hell and Nešetřil (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each 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 H-Coloring can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have short proofs in propositional proof system R^*(log). We complement this upper bound result by a lower bound result for the special example of NP-complete case of the H-Coloring, using the known results about proof complexity of the Pigeonhole Principle