最大充足可能性問題の疎な例題に対する厳密アルゴリズム

Abstract

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^<(1-μ(c))n)>, 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^<O(c)>) 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.