利用树宽进行投影模型计数及其局限性
Exploiting Treewidth for Projected Model Counting and its Limits
摘要：
提出了一种求解投影模型计数（PMC）的新算法. PMC要求计算一个布尔公式相对于一组给定的投影变量的解，其中当限制到投影变量时相同的多个解仅计为一个解。我们的算法利用了输入实例的原始图的小树宽。它在时间上运行$O({2^{2^{k+4}} n^2})$，其中k是树宽，n是实例的输入大小。换句话说，我们得到的问题PMC是固定参数易处理的树宽参数化时。此外，我们考虑到指数时间假设（ETH），并建立有界树宽算法的PMC的下界，产生渐近紧的运行时边界我们的算法。
英文摘要：
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 projected variables, where multiple solutions that are identical when restricted to the projected variables count as only one solution. Our algorithm exploits small treewidth of the primal graph of the input instance. It runs in time $O({2^{2^{k+4}} n^2})$ 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
