[Proof Complexity] new paper

[Азза Гайсин]

Dear colleagues,

my new paper "H-coloring Dichotomy in Proof Complexity"
is available on arxiv.org: https://arxiv.org/abs/2004.13149
Any comments are welcome.

Best regards,
Azza Gaysin

Abstract:
The H-coloring problem can be considered as an example of the computational
problem from a huge class of the constraint satisfaction problems (CSP): an
H-coloring of a graph G is just a homomorphism from G to H and the problem
is to decide for fixed H, given G, if a homomorphism exists or not. The
dichotomy theorem for the 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 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 problem 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), 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 H-coloring problem, using the
known results about proof complexity of the Pigeonhole Principle.