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.MFCS.2021.73
URN: urn:nbn:de:0030-drops-145138
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14513/
Go to the corresponding LIPIcs Volume Portal

Mählmann, Nikolas ; Siebertz, Sebastian ; Vigny, Alexandre

Recursive Backdoors for SAT

pdf-format:
LIPIcs-MFCS-2021-73.pdf (0.9 MB)

Abstract

A strong backdoor in a formula φ of propositional logic to a tractable class C of formulas is a set B of variables of φ such that every assignment of the variables in B results in a formula from C. Strong backdoors of small size or with a good structure, e.g. with small backdoor treewidth, lead to efficient solutions for the propositional satisfiability problem SAT.
In this paper we propose the new notion of recursive backdoors, which is inspired by the observation that in order to solve SAT we can independently recurse into the components that are created by partial assignments of variables. The quality of a recursive backdoor is measured by its recursive backdoor depth. Similar to the concept of backdoor treewidth, recursive backdoors of bounded depth include backdoors of unbounded size that have a certain treelike structure. However, the two concepts are incomparable and our results yield new tractability results for SAT.

BibTeX - Entry

@InProceedings{mahlmann_et_al:LIPIcs.MFCS.2021.73,
  author =	{M\"{a}hlmann, Nikolas and Siebertz, Sebastian and Vigny, Alexandre},
  title =	{{Recursive Backdoors for SAT}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{73:1--73:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14513},
  URN =		{urn:nbn:de:0030-drops-145138},
  doi =		{10.4230/LIPIcs.MFCS.2021.73},
  annote =	{Keywords: Propositional satisfiability SAT, Backdoors, Parameterized Algorithms}
}

Keywords: Propositional satisfiability SAT, Backdoors, Parameterized Algorithms
Collection: 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Issue Date: 2021
Date of publication: 18.08.2021

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