MaxSAT with Absolute Value Functions: A Parameterized Perspective
The natural generalization of the Boolean satisfiability problem to optimization problems is the task of determining the maximum number of clauses that can simultaneously be satisfied in a propositional formula in conjunctive normal form. In the weighted maximum satisfiability problem each clause has a positive weight and one seeks an assignment of maximum weight. The literature almost solely considers the case of positive weights. While the general case of the problem is only restricted slightly by this constraint, many special cases become trivial in the absence of negative weights. In this work we study the problem with negative weights and observe that the problem becomes computationally harder - which we formalize from a parameterized perspective in the sense that various variations of the problem become W[1]-hard if negative weights are present.
Allowing negative weights also introduces new variants of the problem: Instead of maximizing the sum of weights of satisfied clauses, we can maximize the absolute value of that sum. This turns out to be surprisingly expressive even restricted to monotone formulas in disjunctive normal form with at most two literals per clause. In contrast to the versions without the absolute value, however, we prove that these variants are fixed-parameter tractable. As technical contribution we present a kernelization for an auxiliary problem on hypergraphs in which we seek, given an edge-weighted hypergraph, an induced subgraph that maximizes the absolute value of the sum of edge-weights.
parameterized complexity
kernelization
weighted maximum satisfiability
absolute value maximization
Theory of computation~Fixed parameter tractability
12:1-12:20
Regular Paper
https://arxiv.org/abs/2204.12614
Max
Bannach
Max Bannach
Institute for Theoretical Computer Science, Universität zu Lübeck, Germany
https://orcid.org/0000-0002-6475-5512
Pamela
Fleischmann
Pamela Fleischmann
Department of Computer Science, Christian-Albrechts-Universität zu Kiel, Germany
https://orcid.org/0000-0002-1531-7970
Malte
Skambath
Malte Skambath
Department of Computer Science, Christian-Albrechts-Universität zu Kiel, Germany
https://orcid.org/0000-0003-2048-3559
10.4230/LIPIcs.SWAT.2022.12
N. Alon, G.Z. Gutin, E.J. Kim, S. Szeider, and A. Yeo. Solving max-r-SAT above a tight lower bound. Algorithmica, 61(3):638-655, 2011.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, Second Edition, volume 185 of Front. Artif. Intell. Appl. Press, 2021.
J. Chen, C. Xu, and J. Wang. Dealing with 4-variables by resolution: An improved maxsat algorithm. Theor. Comput. Sci., 670:33-44, 2017.
B. Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Inf. Comput., 85(1):12-75, 1990.
Y. Crama, O. Ekin, and P.L. Hammer. Variable and term removal from boolean formulae. Discret. Appl. Math., 75(3):217-230, 1997.
R. Crowston, M. Fellows, G. Gutin, M. Jones, F. Rosamond, S. Thomassé, and A. Yeo. Simultaneously Satisfying Linear Equations Over F₂: MaxLin2 and Max-r-Lin2 Parameterized Above Average. In FSTTCS, volume 13, pages 229-240, 2011.
M. Cygan, F. V. Fomin, L. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized Algorithms. Springer, 2015.
H. Dell, E.J. Kim, M. Lampis, V. Mitsou, and T.Mömke. Complexity and approximability of parameterized max-csps. Algorithmica, 79(1):230-250, 2017.
E. Eiben, R. Ganian, D. Knop, and S. Ordyniak. Unary integer linear programming with structural restrictions. In IJCAI, pages 1284-1290. ijcai.org, 2018.
E. Eiben, R. Ganian, D. Knop, and S. Ordyniak. Solving integer quadratic programming via explicit and structural restrictions. In AAAI, pages 1477-1484. AAAI Press, 2019.
F. Eisenbrand, C. Hunkenschröder, K.M. Klein, M. Koutecký, A. Levin, and S. Onn. An algorithmic theory of integer programming, 2019. URL: http://arxiv.org/abs/1904.01361.
http://arxiv.org/abs/1904.01361
P. Erdős and R. Rado. Intersection theorems for systems of sets. J. London Math. Soc., 1(1):85-90, 1960.
J. Flum and M. Grohe. Parameterized Complexity Theory. EATCS. Springer, 2006.
R. Ganian and S. Ordyniak. Solving integer linear programs by exploiting variable-constraint interactions: A survey. Algorithms, 12(12):248, 2019.
R. Ganian and S. Szeider. New width parameters for model counting. In SAT, volume 10491 of Lecture Notes in Computer Science, pages 38-52. Springer, 2017.
M.R. Garey, D.S. Johnson, and L.J. Stockmeyer. Some simplified np-complete graph problems. Theor. Comput. Sci., 1(3):237-267, 1976.
S. Gaspers and S. Szeider. Kernels for global constraints. In IJCAI, pages 540-545. IJCAI/AAAI, 2011.
S. Gaspers and S. Szeider. Guarantees and limits of preprocessing in constraint satisfaction and reasoning. Artif. Intell., 216:1-19, 2014.
T. Gavenčiak, D. Knop, and M. Koutecký. Integer Programming in Parameterized Complexity: Three Miniatures. In IPEC, volume 115, pages 21:1-21:16, 2019.
T. Gavenčiak, M. Koutecký, and D. Knop. Integer programming in parameterized complexity: Five miniatures. Accepted for Discrete Optimization, 2020. URL: https://doi.org/10.1016/j.disopt.2020.100596.
https://doi.org/10.1016/j.disopt.2020.100596
M. Grohe. The structure of tractable constraint satisfaction problems. In MFCS, volume 4162, pages 58-72. Springer, 2006.
K. Jansen, A. Lassota, and L. Rohwedder. Near-linear time algorithm for n-fold ilps via color coding. SIAM J. Discret. Math., 34(4):2282-2299, 2020.
S. Khanna, M. Sudan, and D.P. Williamson. A complete classification of the approximability of maximization problems derived from boolean constraint satisfaction. In STOC, pages 11-20, 1997.
M. Koutecký, A. Levin, and S. Onn. A Parameterized Strongly Polynomial Algorithm for Block Structured Integer Programs. In ICALP), volume 107 of LIPIcs, pages 85:1-85:14, 2018.
H.W. Lenstra. Integer programming with a fixed number of variables. Math. Oper. Res., 8:538-548, 1983.
M. Mahajan and V. Raman. Parameterizing above guaranteed values: Maxsat and maxcut. J. Algorithms, 31(2):335-354, 1999.
M. Mahajan, V. Raman, and S. Sikdar. Parameterizing above or below guaranteed values. J. Comput. Syst. Sci., 75(2):137-153, 2009.
N. Nishimura, P. Ragde, and S. Szeider. Detecting backdoor sets with respect to horn and binary clauses. In SAT, 2004.
M. Samer and S. Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010.
M. Samer and S. Szeider. Constraint satisfaction with bounded treewidth revisited. J. Comput. Syst. Sci., 76(2):103-114, 2010.
T.J. Schaefer. The complexity of satisfiability problems. In STOC, pages 216-226, 1978.
S. Szeider. The parameterized complexity of k-flip local search for SAT and MAX SAT. Discret. Optim., 8(1):139-145, 2011.
Max Bannach, Pamela Fleischmann, and Malte Skambath
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode