Backdoor Treewidth for SAT

D 2017

Backdoor Treewidth for SAT

GANIAN, Robert, M.S. RAMANUJAN a Stefan SZEIDER

Základní údaje

Originální název

Backdoor Treewidth for SAT

Autoři

GANIAN, Robert (203 Česká republika, garant, domácí), M.S. RAMANUJAN (356 Indie) a Stefan SZEIDER (40 Rakousko)

Vydání

10491. vyd. Nemecko, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, od s. 20-37, 18 s. 2017

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/17:00100551

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-66262-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-66263-3_2

UT WoS

000455337600002

Klíčová slova anglicky

Treewidth; Parameterized Complexity; SAT; Backdoors

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2020 11:43, Mgr. Michal Petr

Anotace

V originále

A strong backdoor in a CNF formula is a set of variables such that each possible instantiation of these variables moves the formula into a tractable class. The algorithmic problem of finding a strong backdoor has been the subject of intensive study, mostly within the parameterized complexity framework. Results to date focused primarily on backdoors of small size. In this paper we propose a new approach for algorithmically exploiting strong backdoors for SAT: instead of focusing on small backdoors, we focus on backdoors with certain structural properties. In particular, we consider backdoors that have a certain tree-like structure, formally captured by the notion of backdoor treewidth. First, we provide a fixed-parameter algorithm for SAT parameterized by the backdoor treewidth w.r.t. the fundamental tractable classes Horn, Anti-Horn, and 2CNF. Second, we consider the more general setting where the backdoor decomposes the instance into components belonging to different tractable classes, albeit focusing on backdoors of treewidth 1 (i.e., acyclic backdoors). We give polynomial-time algorithms for SAT and #SAT for instances that admit such an acyclic backdoor.

Citovat

GANIAN, Robert, M.S. RAMANUJAN a Stefan SZEIDER. Backdoor Treewidth for SAT. Online. In Serge Gaspers and Toby Walsh. Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. 10491. vyd. Nemecko: Springer, 2017, s. 20-37. ISBN 978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3_2.

@inproceedings{1414044,
   author = {Ganian, Robert and Ramanujan, M.S. and Szeider, Stefan},
   address = {Nemecko},
   booktitle = {Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-319-66263-3_2},
   edition = {10491},
   editor = {Serge Gaspers and Toby Walsh},
   keywords = {Treewidth; Parameterized Complexity; SAT; Backdoors},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Nemecko},
   isbn = {978-3-319-66262-6},
   pages = {20-37},
   publisher = {Springer},
   title = {Backdoor Treewidth for SAT},
   url = {https://link.springer.com/chapter/10.1007/978-3-319-66263-3_2},
   year = {2017}
}

TY  - JOUR
ID  - 1414044
AU  - Ganian, Robert - Ramanujan, M.S. - Szeider, Stefan
PY  - 2017
TI  - Backdoor Treewidth for SAT
PB  - Springer
CY  - Nemecko
SN  - 9783319662626
KW  - Treewidth
KW  - Parameterized Complexity
KW  - SAT
KW  - Backdoors
UR  - https://link.springer.com/chapter/10.1007/978-3-319-66263-3_2
L2  - https://link.springer.com/chapter/10.1007/978-3-319-66263-3_2
N2  - A strong backdoor in a CNF formula is a set of variables such that each possible instantiation of these variables moves the formula into a tractable class. The algorithmic problem of finding a strong backdoor has been the subject of intensive study, mostly within the parameterized complexity framework. Results to date focused primarily on backdoors of small size. In this paper we propose a new approach for algorithmically exploiting strong backdoors for SAT: instead of focusing on small backdoors, we focus on backdoors with certain structural properties. In particular, we consider backdoors that have a certain tree-like structure, formally captured by the notion of backdoor treewidth. First, we provide a fixed-parameter algorithm for SAT parameterized by the backdoor treewidth w.r.t. the fundamental tractable classes Horn, Anti-Horn, and 2CNF. Second, we consider the more general setting where the backdoor decomposes the instance into components belonging to different tractable classes, albeit focusing on backdoors of treewidth 1 (i.e., acyclic backdoors). We give polynomial-time algorithms for SAT and #SAT for instances that admit such an acyclic backdoor.
ER  -

GANIAN, Robert, M.S. RAMANUJAN a Stefan SZEIDER. Backdoor Treewidth for SAT. Online. In Serge Gaspers and Toby Walsh. \textit{Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings}. 10491. vyd. Nemecko: Springer, 2017, s.~20-37. ISBN~978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3\_{}2.

Podrobný výpis o publikaci