In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projection variables, where multiple solutions that are identical when restricted to the projection variables count as only one solution. Inspired by the observation that the so-called "treewidth" is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance. More precisely, it runs in time O(2^2k+4n2) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm. While the algorithm above serves as a first theoretical upper bound and although it might be quite appealing for small values of k, unsurprisingly a naive implementation adhering to this runtime bound suffers already from instances of relatively small width. Therefore, we turn our attention to several measures in order to resolve this issue towards exploiting treewidth in practice: We present a technique called nested dynamic programming, where different levels of abstractions of the primal graph are used to (recursively) compute and refine tree decompositions of a given instance. Finally, we provide a nested dynamic programming algorithm and an implementation that relies on database technology for PMC and a prominent special case of PMC, namely model counting (#Sat). Experiments indicate that the advancements are promising, allowing us to solve instances of treewidth upper bounds beyond 200.

翻译：本文提出了一种新颖算法来解决投影模型计数（PMC）问题。PMC要求计算布尔公式在给定投影变量集上的解数量，其中多个在投影变量上相同的解仅计为一个解。受所谓"树宽"是最突出的结构参数之一的观察启发，我们的算法利用了输入实例原始图的小树宽特性。具体而言，该算法运行时间为O(2^(2k+4)n^2)，其中k为树宽，n为实例的输入规模。换言之，我们证明了当以树宽为参数时，PMC问题是固定参数可处理的。此外，我们考虑指数时间假说（ETH），建立了PMC有界树宽算法的下界，从而得出算法渐近紧致的运行时间边界。尽管上述算法作为首个理论上的上界，且对于较小的k值可能颇具吸引力，但不出所料，遵循该运行时间边界的简单实现即使在树宽较小的实例上也会遇到困难。因此，我们转向若干措施以解决该问题，从而在实践中利用树宽：我们提出一种称为嵌套动态规划的技术，利用原始图的不同抽象层次来（递归地）计算和精化给定实例的树分解。最后，我们为PMC及其重要特例——模型计数（#Sat）提供了嵌套动态规划算法及依赖于数据库技术的实现。实验表明这些进展颇具前景，使我们能够求解树宽上界超过200的实例。