Improved Algorithms for Maximum Satisfiability and Its Special Cases
Kirill Brilliantov, Vasily Alferov, Ivan Bliznets
Abstract
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.
BibTeX
@article{Brilliantov_Alferov_Bliznets_2023, title={Improved Algorithms for Maximum Satisfiability and Its Special Cases}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25503}, DOI={10.1609/aaai.v37i4.25503}, abstractNote={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.}, number={4}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Brilliantov, Kirill and Alferov, Vasily and Bliznets, Ivan}, year={2023}, month={Jun.}, pages={3898-3905} }