License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.19
URN: urn:nbn:de:0030-drops-166934
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16693/
Go to the corresponding LIPIcs Volume Portal

Bannach, Max ; Skambath, Malte ; Tantau, Till

On the Parallel Parameterized Complexity of MaxSAT Variants

pdf-format:
LIPIcs-SAT-2022-19.pdf (0.8 MB)

Abstract

In the maximum satisfiability problem (max-sat) we are given a propositional formula in conjunctive normal form and have to find an assignment that satisfies as many clauses as possible. We study the parallel parameterized complexity of various versions of max-sat and provide the first constant-time algorithms parameterized either by the solution size or by the allowed excess relative to some guarantee ("above guarantee" versions). For the dual parameterized version where the parameter is the number of clauses we are allowed to leave unsatisfied, we present the first parallel algorithm for max-2sat (known as almost-2sat). The difficulty in solving almost-2sat in parallel comes from the fact that the iterative compression method, originally developed to prove that the problem is fixed-parameter tractable at all, is inherently sequential. We observe that a graph flow whose value is a parameter can be computed in parallel and use this fact to develop a parallel algorithm for the vertex cover problem parameterized above the size of a given matching. Finally, we study the parallel complexity of max-sat parameterized by the vertex cover number, the treedepth, the feedback vertex set number, and the treewidth of the input’s incidence graph. While max-sat is fixed-parameter tractable for all of these parameters, we show that they allow different degrees of possible parallelization. For all four we develop dedicated parallel algorithms that are constructive, meaning that they output an optimal assignment - in contrast to results that can be obtained by parallel meta-theorems, which often only solve the decision version.

BibTeX - Entry

@InProceedings{bannach_et_al:LIPIcs.SAT.2022.19,
  author =	{Bannach, Max and Skambath, Malte and Tantau, Till},
  title =	{{On the Parallel Parameterized Complexity of MaxSAT Variants}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16693},
  URN =		{urn:nbn:de:0030-drops-166934},
  doi =		{10.4230/LIPIcs.SAT.2022.19},
  annote =	{Keywords: max-sat, almost-sat, parallel algorithms, fixed-parameter tractability}
}

Keywords: max-sat, almost-sat, parallel algorithms, fixed-parameter tractability
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI