ASP中树宽感知的复杂性：并非所有正循环都是同样困难的
Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard
摘要：
标准答案集程序（ASP）的一致性判定是NP-完全的，与经典命题逻辑（SAT）的满意度问题一样困难。解决这些问题的最佳算法在最坏的情况下需要指数时间。指数时间假设（ETH）意味着这个结果对于SAT是紧的，也就是说，SAT不能在亚指数时间内求解。这立即确定了结果对于ASP的一致性问题也是紧的。然而，考虑到问题的树宽，ASP的一致性问题比SAT稍微困难一些：虽然SAT可以通过在树宽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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
