论文标题
ASP中的树宽感知复杂性：并非所有正循环都同样难
Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard
论文作者
论文摘要
众所周知，确定正常答案集程序（ASP）的一致性是NP的完整性，因此，与经典命题逻辑（SAT）的满意度问题一样困难。解决这些问题的最佳算法在最坏的情况下需要指数时间。指数时间假设（ETH）意味着SAT的结果很紧，也就是说，SAT不能以次指数时间解决。这立即确定结果对于ASP的一致性问题也很紧。但是，考虑到问题的树宽，ASP的一致性问题比SAT要困难得多：尽管SAT可以通过在TreeWidth K中以指数时间运行的算法来求解，但最近显示ASP需要在K \ CDOT LOG（K）中进行指数时间。这笔额外的成本应得检查是否由于程序中的积极周期没有自支撑的真原子。在本文中，我们完善了上述结果，并表明ASP的一致性问题可以在k \ cdot log（λ）的指数时间内解决，其中λ是该程序的正依赖性图中最大的最大较大牢固连接组件之间的最小值。我们提供了一种动态编程算法，该算法解决了问题，并从ASP到SAT缩小了粘附于上述限制。
It is well-know that deciding consistency for normal answer set programs (ASP) is NP-complete, thus, as hard as the satisfaction problem for classical propositional logic (SAT). The best algorithms to solve these problems take exponential time in the worst case. The exponential time hypothesis (ETH) implies that this result is tight for SAT, that is, SAT cannot be solved in subexponential time. This immediately establishes that the result is also tight for the consistency problem for ASP. However, accounting for the treewidth of the problem, the consistency problem for ASP is slightly harder than SAT: while SAT can be solved by an algorithm that runs in exponential time in the treewidth k, it was recently shown that ASP requires exponential time in k \cdot log(k). This extra cost is due checking that there are no self-supported true atoms due to positive cycles in the program. In this paper, we refine the above result and show that the consistency problem for ASP can be solved in exponential time in k \cdot log(λ) where λ is the minimum between the treewidth and the size of the largest strongly-connected component in the positive dependency graph of the program. We provide a dynamic programming algorithm that solves the problem and a treewidth-aware reduction from ASP to SAT that adhere to the above limit.
