H-colouring dichotomy in proof complexity

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F21%3A10437362" target="_blank" >RIV/00216208:11320/21:10437362 - isvavai.cz</a>

Výsledek na webu

<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=j6FeGlE1dk" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=j6FeGlE1dk</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1093/logcom/exab028" target="_blank" >10.1093/logcom/exab028</a>

Jazyk výsledku

angličtina

Název v původním jazyce

H-colouring dichotomy in proof complexity

Popis výsledku v původním jazyce

The H-colouring problem for undirected simple graphs is a computational problem from a huge class of the constraint satisfaction problems (CSPs): an H-colouring 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-colouring problem was proved by Hell and Nesetril (1990, J Comb. Theory Ser. B, 48, 92-110) (an analogous theorem for all CSPs was recently proved by Zhuk (2020, J. ACM, 67, 1-78) and Bulatov (2017, FOCS, 58, 319-330)), 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-colouring problem can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have polynomial 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. This upper bound follows also from a different construction in [1]. 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-colouring problem, using known results about the proof complexity of the pigeonhole principle. The main goal of our work is to start the development of some of the theories beyond the CSP dichotomy theorem in bounded arithmetic. We aim eventually in a subsequent work to formalize in such a theory the soundness of Zhuk&apos;s algorithm, extending the upper bound proved here from undirected simple graphs to the general case of directed graphs in some logical calculi.

Název v anglickém jazyce

H-colouring dichotomy in proof complexity

Popis výsledku anglicky

The H-colouring problem for undirected simple graphs is a computational problem from a huge class of the constraint satisfaction problems (CSPs): an H-colouring 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-colouring problem was proved by Hell and Nesetril (1990, J Comb. Theory Ser. B, 48, 92-110) (an analogous theorem for all CSPs was recently proved by Zhuk (2020, J. ACM, 67, 1-78) and Bulatov (2017, FOCS, 58, 319-330)), 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-colouring problem can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have polynomial 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. This upper bound follows also from a different construction in [1]. 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-colouring problem, using known results about the proof complexity of the pigeonhole principle. The main goal of our work is to start the development of some of the theories beyond the CSP dichotomy theorem in bounded arithmetic. We aim eventually in a subsequent work to formalize in such a theory the soundness of Zhuk&apos;s algorithm, extending the upper bound proved here from undirected simple graphs to the general case of directed graphs in some logical calculi.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of Logic and Computation

ISSN

0955-792X

e-ISSN

—

Svazek periodika

2021

Číslo periodika v rámci svazku

31

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

20

Strana od-do

1206-1225

Kód UT WoS článku

000687199700002

EID výsledku v databázi Scopus

2-s2.0-85113772399