一句话：证明超图分离定理，并据此给出变量频率受限 CSP 的亚指数时间 SAT、#SAT、MaxSAT 算法及 resolution 反驳。
本文研究变量频率有界的 CSP 的 SAT、计数与优化。作者证明超图分离定理：任意 r-均匀超图若最大顶点度为 o(√m)，则可删去至多 (1/2−ε_r)m 条边，使各连通分量至多含 m/2 条边。基于此，他们给出运行时间 d^{(1−ε_r)m} 的算法，判定 m 变量 (d,k)-CSP 可满足性；每个变量至多出现在 r 个约束中，k∈o(√m)，ε_r 仅依赖 r，算法也求解 #CSP-SAT 与 Max-CSP-SAT。此外，不可满足且变量频率为 r 的 (2,k)-CSP 的 CNF 可在树状 resolution 中以 2^{(1−ε_r)m} 大小反驳；对度至多 k 的图上 Tseitin 公式给出确定性反驳算法。
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.
@article{paperbot1258,
title = {A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm},
author = {Michal Koucký and Vojtěch Rödl and Navid Talebanfard},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:17)2021}
}