A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth

The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of [Formula: see text]. We improv...

Descripción completa

Detalles Bibliográficos
Autores principales: Slivovsky, Friedrich, Szeider, Stefan
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326555/
http://dx.doi.org/10.1007/978-3-030-51825-7_19
_version_ 1783552369830658048
author Slivovsky, Friedrich
Szeider, Stefan
author_facet Slivovsky, Friedrich
Szeider, Stefan
author_sort Slivovsky, Friedrich
collection PubMed
description The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of [Formula: see text]. We improve this factor to [Formula: see text] by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails.
format Online
Article
Text
id pubmed-7326555
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73265552020-07-01 A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth Slivovsky, Friedrich Szeider, Stefan Theory and Applications of Satisfiability Testing – SAT 2020 Article The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of [Formula: see text]. We improve this factor to [Formula: see text] by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails. 2020-06-26 /pmc/articles/PMC7326555/ http://dx.doi.org/10.1007/978-3-030-51825-7_19 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Slivovsky, Friedrich
Szeider, Stefan
A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title_full A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title_fullStr A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title_full_unstemmed A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title_short A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
title_sort faster algorithm for propositional model counting parameterized by incidence treewidth
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326555/
http://dx.doi.org/10.1007/978-3-030-51825-7_19
work_keys_str_mv AT slivovskyfriedrich afasteralgorithmforpropositionalmodelcountingparameterizedbyincidencetreewidth
AT szeiderstefan afasteralgorithmforpropositionalmodelcountingparameterizedbyincidencetreewidth
AT slivovskyfriedrich fasteralgorithmforpropositionalmodelcountingparameterizedbyincidencetreewidth
AT szeiderstefan fasteralgorithmforpropositionalmodelcountingparameterizedbyincidencetreewidth

Ejemplares similares