2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/124269We 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.9 pages, 1 figureData Structures and AlgorithmsComputational ComplexityLogic in Computer ScienceF.2.2; F.4.1text