Improved Exact Algorithms for Max-Sat

 

In this talk we present improved exact and parameterized algorithms for the maximum satisfiability problem. In particular, we give an algorithm that computes a truth assignment for a boolean formula F satisfying the maximum number of clauses in time O(1.3247^m |F|), where m is the number of clauses in F, and |F| is the sum of the number of literals appearing in each clause in F. Moreover, given a parameter k, we give an O(1.3695^k k^2 + |F|) parameterized algorithm that decides whether a truth assignment for F satisfying at least k clauses exists.