A SEPARATOR THEOREM FOR HYPERGRAPHS AND A CSP-SAT ALGORITHM

Abstract

We show that for every r ≥ 2 there exists ɛr > 0 such that any r-uniform hypergraph with m edges and maximum vertex degree o(√m) contains a set of at most (1 − ɛr)m edges the removal of which breaks the hypergraph into connected components 2 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.