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

摘要

We present a moderately exponential time and polynomial space algorithm for sparse instances of Max SAT. Our algorithms run in time of the form for instances with n variables and cn clauses. Our deterministic and randomized algorithm achieve and respectively. Previously, an exponential space deterministic algorithm with was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space deterministic algorithm with 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.