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

We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. For instances with n variables and cn clauses, our algorithm runs in time O(2^, where μ(c) = O(1/c^2log^2 c). Previously, an exponential space algorithm with μ(c) = O(1/clog c) was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space algorithm with μ(c) = O(1/2^) was shown by Kulikov and Kutzkov [CSR 2007]. Our algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam