A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and Its Algorithmic Application.

For a formula F in conjunctive normal form (CNF), let sat(F) be the maximum number of clauses of F that can be satisfied by a truth assignment, and let m be the number of clauses in F. It is well-known that for every CNF formula F, sat(F) ≥ m/2 and the bound is tight when F consists of conflicting unit clauses (x) and ]> . Since each truth assignment satisfies exactly one clause in each pair of conflicting unit clauses, it is natural to reduce F to the unit-conflict free (UCF) form. If F is UCF, then Lieberherr and Specker (J. ACM 28(2):411-421, 1981) proved that ]> , where ]> . We introduce another reduction that transforms a UCF CNF formula F into a UCF CNF formula F', which has a complete matching, i.e., there is an injective map from the variables to the clauses, such that each variable maps to a clause containing that variable or its negation. The formula F' is obtained from F by deleting some clauses and the variables contained only in the deleted clauses. We prove that ]> , where n' and m' are the number of variables and clauses in F', respectively. This improves the Lieberherr-Specker lower bound on sat(F). We show that our new bound has an algorithmic application by considering the following parameterized problem: given a UCF CNF formula F decide whether sat(F) ]> where k is the parameter. This problem was introduced by Mahajan and Raman (J. Algorithms 31(2):335–354, 1999) who conjectured that the problem is fixed-parameter tractable, i.e., it can be solved in time f(k)(nm)^O(1) for some computable function f of k only. We use the new bound to show that the problem is indeed fixed-parameter tractable by describing a polynomial-time algorithm that transforms any problem instance into an equivalent one with at most ]> variables. [ABSTRACT FROM AUTHOR]