New upper bounds for maxsat

Abstract

Given a boolean formula F in conjunctive normal form and an integer k, is there a truth assignment satisfying at least k clauses? This is the decision version of the Maximum Satisfiability (MaxSat) problem we study in this paper. We improve upper bounds on the worst case running time for MaxSat. First, Cai and Chen showed that MaxSat can be solved in time /F/2O(k) when the clause size is bounded by a constant. Imposing no restrictions on clause size, Mahajan and Raman and, independently, Dantsin et al. improved this to O(/F/φk), where φ ≈1:6181 is the golden ratio. We present an algorithm running in time O(/F/1:3995k). The result extends to finding an optimal assignment and has several applications, in particular, for parameterized complexity and approximation algorithms. Moreover, if F has K clauses, we can find an optimal assignment in O(/F/1:3972K) steps and in O(1:1279/F/) steps, respectively. These are the fastest algorithm in the number of clauses and the length of the formula, respectively. © Springer-Verlag Berlin Heidelberg 1999.