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.