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的实例。