Satisfiability of acyclic and almost acyclic CNF formulas

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

ORDYNIAK Sebastian PAULUSMA Daniel SZEIDER Stefan

Rok publikování 2013
Druh Článek v odborném periodiku
Časopis / Zdroj Theoretical Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1016/j.tcs.2012.12.039
Obor Teorie informace
Klíčová slova Acyclic hypergraph; Chordal bipartite graph; Davis-Putnam resolution
Popis We show that the SATISFIABILITY (SAT) problem for CNF formulas with beta-acyclic hypergraphs can be solved in polynomial time by using a special type of Davis-Putnam resolution in which each resolvent is a subset of a parent clause. We extend this class to CNF formulas for which this type of Davis-Putnam resolution still applies and show that testing membership in this class is NP-complete. We compare the class of beta-acyclic formulas and this superclass with a number of known polynomial formula classes. We then study the parameterized complexity of SAT for "almost" beta-acyclic instances, using as parameter the formula's distance from being beta-acyclic. As distance we use the size of a smallest strong backdoor set and the beta-hypertree width. As a by-product we obtain the W[1]-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve. (C) 2013 Elsevier B.V. All rights reserved.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.