Backdoor Treewidth for SAT

D 2017

Backdoor Treewidth for SAT

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

Basic information

Original name

Backdoor Treewidth for SAT

Authors

GANIAN, Robert (203 Czech Republic, guarantor, belonging to the institution), M.S. RAMANUJAN (356 India) and Stefan SZEIDER (40 Austria)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Germany

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/17:00100551

Organization unit

Faculty of Informatics

ISBN

978-3-319-66262-6

ISSN

DOI

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

UT WoS

000455337600002

Keywords in English

Treewidth; Parameterized Complexity; SAT; Backdoors

Abstract

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 and 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. 10491st ed. Nemecko: Springer, 2017, p. 20-37. ISBN 978-3-319-66262-6. Available from: 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 and 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}. 10491st ed. Nemecko: Springer, 2017, p.~20-37. ISBN~978-3-319-66262-6. Available from: https://dx.doi.org/10.1007/978-3-319-66263-3\_{}2.

Detailed Information on Publication Record