Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph

In the paper, we study the Maximum Satisfiability and the Partial Maximum Satisfiability problems. Using Gallai–Edmonds decomposition, we significantly improve the upper bound for the Maximum Satisfiability problem parameterized above maximum matching in the variable-clause graph. Our algorithm operates with a runtime of O*(2.83^k'), a substantial improvement compared to the previous approach requiring O*(4^k' ), where k' denotes the relevant parameter. Moreover, this result immediately implies O*(1.14977^m) and O*(1.27895^m) time algorithms for the (n, 3)-MaxSAT and (n, 4)-MaxSAT where m is the overall number of clauses. These upper bounds improve prior-known upper bounds equal to O*(1.1554^m) and O*(1.2872^m). We also adapt the algorithm so that it can handle instances of Partial Maximum Satisfiability without losing performance in some cases. Note that this is somewhat surprising, as the existence of even one hard clause can significantly increase the hardness of a problem.

Authors

• Vasily Alferov Independent Researcher
• Ivan Bliznets University of Groningen
• Kirill Brilliantov St. Petersburg Department of Steklov Mathematical Institute of the RAS

Keywords

• CSO: Constraint Optimization
• CSO: Constraint Satisfaction
• CSO: Other Foundations of Constraint Satisfaction
• CSO: Satisfiability