Improved Algorithms for Maximum Satisfiability and Its Special Cases

The Maximum Satisfiability (MAXSAT) problem is an optimization version of the Satisfiability problem (SAT) in which one is given a CNF formula with n variables and needs to find the maximum number of simultaneously satisfiable clauses. Recent works achieved significant progress in proving new upper bounds on the worst-case computational complexity of MAXSAT. All these works reduce general MAXSAT to a special case of MAXSAT where each variable appears a small number of times. So, it is important to design fast algorithms for (n, k)-MAXSAT to construct an efficient exact algorithm for MAXSAT. (n, k)-MAXSAT is a special case of MAXSAT where each variable appears at most k times in the input formula. For the (n, 3)-MAXSAT problem, we design a O * (1.1749 n ) algorithm improving on the previous record running time of O * (1.191 n ). For the (n, 4)-MAXSAT problem, we construct a O * (1.3803 n ) algorithm improving on the previous best running time of O * (1.4254 n ). Using the results, we develop a O * (1.0911 L ) algorithm for the MAXSAT where L is a length of the input formula which improves previous algorithm with O * (1.0927 L ) running time.