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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10200 1.2 Computer and information sciences
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-66263-3_2
UT WoS 000455337600002
Keywords in English Treewidth; Parameterized Complexity; SAT; Backdoors
Tags core_A, firank_A
Tags International impact, Reviewed
Changed by Changed by: Mgr. Michal Petr, učo 65024. Changed: 28/4/2020 11:43.
Abstract
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.
PrintDisplayed: 20/9/2024 07:23