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 (x). 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 sat(F) > φm, where φ = ( 5~(1/2) - l)/2.rnWe 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 sat(F) > φm + (1 - φ)(m - m') + n'(2 - 3φ)/2, where n' and m' are the number of variables and clauses in F', respectively. This improves the Lieberherr-Specker lower bound on sat(F).rnWe 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) > φm + k, 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 fik){nm)~0(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 [(7 + 3 5(1/2))k] variables.