A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm
We show that for every $r \ge 2$ there exists $\epsilon_r > 0$ such that any $r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$ contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of which breaks the hypergraph into connected components with at mos...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7484/pdf |
| _version_ | 1797268533263990784 |
|---|---|
| author | Michal Koucký Vojtěch Rödl Navid Talebanfard |
| author_facet | Michal Koucký Vojtěch Rödl Navid Talebanfard |
| author_sort | Michal Koucký |
| collection | DOAJ |
| description | We show that for every $r \ge 2$ there exists $\epsilon_r > 0$ such that any
$r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$
contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of
which breaks the hypergraph into connected components with at most $m/2$ edges.
We use this to give an algorithm running in time $d^{(1 - \epsilon_r)m}$ that
decides satisfiability of $m$-variable $(d, k)$-CSPs in which every variable
appears in at most $r$ constraints, where $\epsilon_r$ depends only on $r$ and
$k\in o(\sqrt{m})$. Furthermore our algorithm solves the corresponding #CSP-SAT
and Max-CSP-SAT of these CSPs. We also show that CNF representations of
unsatisfiable $(2, k)$-CSPs with variable frequency $r$ can be refuted in
tree-like resolution in size $2^{(1 - \epsilon_r)m}$. Furthermore for Tseitin
formulas on graphs with degree at most $k$ (which are $(2, k)$-CSPs) we give a
deterministic algorithm finding such a refutation. |
| first_indexed | 2024-04-25T01:33:59Z |
| format | Article |
| id | doaj.art-f63b1b3c4f7540ba83231ccde9a3b0b3 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:59Z |
| publishDate | 2021-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-f63b1b3c4f7540ba83231ccde9a3b0b32024-03-08T10:35:55ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-12-01Volume 17, Issue 410.46298/lmcs-17(4:17)20217484A Separator Theorem for Hypergraphs and a CSP-SAT AlgorithmMichal Kouckýhttps://orcid.org/0000-0003-0808-2269Vojtěch RödlNavid Talebanfardhttps://orcid.org/0000-0002-3524-9282We show that for every $r \ge 2$ there exists $\epsilon_r > 0$ such that any $r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$ contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of which breaks the hypergraph into connected components with at most $m/2$ edges. We use this to give an algorithm running in time $d^{(1 - \epsilon_r)m}$ that decides satisfiability of $m$-variable $(d, k)$-CSPs in which every variable appears in at most $r$ constraints, where $\epsilon_r$ depends only on $r$ and $k\in o(\sqrt{m})$. Furthermore our algorithm solves the corresponding #CSP-SAT and Max-CSP-SAT of these CSPs. We also show that CNF representations of unsatisfiable $(2, k)$-CSPs with variable frequency $r$ can be refuted in tree-like resolution in size $2^{(1 - \epsilon_r)m}$. Furthermore for Tseitin formulas on graphs with degree at most $k$ (which are $(2, k)$-CSPs) we give a deterministic algorithm finding such a refutation.https://lmcs.episciences.org/7484/pdfcomputer science - logic in computer sciencecomputer science - computational complexity |
| spellingShingle | Michal Koucký Vojtěch Rödl Navid Talebanfard A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm Logical Methods in Computer Science computer science - logic in computer science computer science - computational complexity |
| title | A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm |
| title_full | A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm |
| title_fullStr | A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm |
| title_full_unstemmed | A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm |
| title_short | A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm |
| title_sort | separator theorem for hypergraphs and a csp sat algorithm |
| topic | computer science - logic in computer science computer science - computational complexity |
| url | https://lmcs.episciences.org/7484/pdf |
| work_keys_str_mv | AT michalkoucky aseparatortheoremforhypergraphsandacspsatalgorithm AT vojtechrodl aseparatortheoremforhypergraphsandacspsatalgorithm AT navidtalebanfard aseparatortheoremforhypergraphsandacspsatalgorithm AT michalkoucky separatortheoremforhypergraphsandacspsatalgorithm AT vojtechrodl separatortheoremforhypergraphsandacspsatalgorithm AT navidtalebanfard separatortheoremforhypergraphsandacspsatalgorithm |