A SEPARATOR THEOREM FOR HYPERGRAPHS AND A CSP-SAT ALGORITHM

We show that for every r >= 2 there exists epsilon(r) > 0 such that any r-uniform hypergraph with m edges and maximum vertex degree o(root m) contains a set of at most (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 is an element of o(root 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.