首页    期刊浏览 2024年12月03日 星期二
登录注册

文章基本信息

  • 标题:A SEPARATOR THEOREM FOR HYPERGRAPHS AND A CSP-SAT ALGORITHM
  • 本地全文:下载
  • 作者:Michal Koucký ; Vojtěch Rödl ; Navid Talebanfard
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2021
  • 卷号:17
  • 期号:4
  • 页码:1-14
  • DOI:10.46298/lmcs-17(4:17)2021
  • 语种:English
  • 出版社:Technical University of Braunschweig
  • 摘要: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.
  • 关键词:CSP-SAT;hypergraph;separator;resolution;Tseitin formulas
国家哲学社会科学文献中心版权所有