Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction

ABSTRACT. We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. Our algorithms run in time of the form $O(2^{(1-\mu(c))n})$ for instances with $n$ variables and $cn$ clauses. Our deterministic and randomized algorithm achieve $\mu(c) = \Omega(\frac{1}{c^2\log^2 c})$ and $\mu(c) = \Omega(\frac{1}{c \log^3 c})$ respectively. Previously, an exponential space deterministic algorithm with $\mu(c) = \Omega(\frac{1}{c\log c})$ was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space deterministic algorithm with $\mu(c) = \Omega(\frac{1}{2^{O(c)}})$ was shown by Kulikov and Kutzkov [CSR 2007].

Our algorithms have three new features. They can handle instances with (1) weights and (2) hard constraints, and also (3) they can solve counting versions of Max SAT. Our deterministic algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam. Our randomized algorithm uses random restriction instead of greedy restriction.