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.ESA.2022.46
URN: urn:nbn:de:0030-drops-169840
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16984/
Go to the corresponding LIPIcs Volume Portal

Dreier, Jan ; Ordyniak, Sebastian ; Szeider, Stefan

SAT Backdoors: Depth Beats Size

pdf-format:
LIPIcs-ESA-2022-46.pdf (0.9 MB)

Abstract

For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) and Krom (i.e., 2CNF) formulas (Dowling and Gallier, 1984). Backdoors, introduced by Williams, Gomes and Selman (2003), gradually extend such a tractable class to all formulas of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a formula and a tractable class. Backdoor depth, introduced by Mählmann, Siebertz, and Vigny (2021), is a more refined distance measure, which admits the utilization of different backdoor variables in parallel. Bounded backdoor size implies bounded backdoor depth, but there are formulas of constant backdoor depth and arbitrarily large backdoor size.
We propose FPT approximation algorithms to compute backdoor depth into the classes Horn and Krom. This leads to a linear-time algorithm for deciding the satisfiability of formulas of bounded backdoor depth into these classes. We base our FPT approximation algorithm on a sophisticated notion of obstructions, extending Mählmann et al.’s obstruction trees in various ways, including the addition of separator obstructions. We develop the algorithm through a new game-theoretic framework that simplifies the reasoning about backdoors.
Finally, we show that bounded backdoor depth captures tractable classes of CNF formulas not captured by any known method.

BibTeX - Entry

@InProceedings{dreier_et_al:LIPIcs.ESA.2022.46,
  author =	{Dreier, Jan and Ordyniak, Sebastian and Szeider, Stefan},
  title =	{{SAT Backdoors: Depth Beats Size}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{46:1--46:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16984},
  URN =		{urn:nbn:de:0030-drops-169840},
  doi =		{10.4230/LIPIcs.ESA.2022.46},
  annote =	{Keywords: satisfiability, backdoor (depth)}
}

Keywords: satisfiability, backdoor (depth)
Collection: 30th Annual European Symposium on Algorithms (ESA 2022)
Issue Date: 2022
Date of publication: 01.09.2022

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