A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm
share
We show that for every r ≥ 2 there exists ϵ_r > 0 such that any r-uniform hypergraph on m edges with bounded vertex degree has a set of at most (1/2 - ϵ_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 - ϵ_r)m that decides satisfiability of m-variable (d, k)-CSPs in which every variable appears in at most r constraints, where ϵ_r depends only on r and k∈ o(√(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 - ϵ_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.
READ FULL TEXT