Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911048763703296 |
|---|---|
| author | Berkholz, Christoph Lichter, Moritz Vinall-Smeeth, Harry |
| author_facet | Berkholz, Christoph Lichter, Moritz Vinall-Smeeth, Harry |
| contents | We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz (TOCL 2023) showed that there is a resolution refutation of narrow width $k$ for two graphs if and only if they can be distinguished in ($k+1$)-variable first-order logic (FO$^{k+1}$) and hence by a count-free variant of the $k$-dimensional Weisfeiler-Leman algorithm. While DAG-like narrow width $k$ resolution refutations have size at most $n^k$, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width $k$ but only in tree-like size $2^{Ω(n^{k/2})}$. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical width versus tree-like size trade-off by Razborov (JACM 2016). To prove our result, we develop a new variant of the $k$-pebble EF-game for FO$^k$ to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on a modified variant of the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer (FOCS 2023). Using a recent improved robust compressed CFI construction of Janett, Nordström, and Pang (unpublished manuscript), we obtain a similar bound for width $k$ (instead of the stronger but less common narrow width) and make the result more robust. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_17947 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism Berkholz, Christoph Lichter, Moritz Vinall-Smeeth, Harry Logic in Computer Science Computational Complexity We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz (TOCL 2023) showed that there is a resolution refutation of narrow width $k$ for two graphs if and only if they can be distinguished in ($k+1$)-variable first-order logic (FO$^{k+1}$) and hence by a count-free variant of the $k$-dimensional Weisfeiler-Leman algorithm. While DAG-like narrow width $k$ resolution refutations have size at most $n^k$, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width $k$ but only in tree-like size $2^{Ω(n^{k/2})}$. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical width versus tree-like size trade-off by Razborov (JACM 2016). To prove our result, we develop a new variant of the $k$-pebble EF-game for FO$^k$ to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on a modified variant of the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer (FOCS 2023). Using a recent improved robust compressed CFI construction of Janett, Nordström, and Pang (unpublished manuscript), we obtain a similar bound for width $k$ (instead of the stronger but less common narrow width) and make the result more robust. |
| title | Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism |
| topic | Logic in Computer Science Computational Complexity |
| url | https://arxiv.org/abs/2407.17947 |