arXiv · cs/0610174
A Fixed-Parameter Algorithm for #SAT with Parameter Incidence Treewidth
Abstract
We present an efficient fixed-parameter algorithm for #SAT parameterized by the incidence treewidth, i.e., the treewidth of the bipartite graph whose vertices are the variables and clauses of the given CNF formula; a variable and a clause are joined by an edge if and only if the variable occurs in the clause. Our algorithm runs in time O(4^k k l N), where k denotes the incidence treewidth, l denotes the size of a largest clause, and N denotes the number of nodes of the tree-decomposition.
Explore related subjects
Keep this discovery
Marko Samer, Stefan Szeider. 2007-02-21. A Fixed-Parameter Algorithm for #SAT with Parameter Incidence Treewidth. https://arxiv.org/abs/cs/0610174
Cite the original work for its findings. Save a collection to share your selection of sources.