论文标题
width感知的正常ASP降低了SAT-正常的ASP比SAT难吗？
Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?
论文作者
论文摘要
答案集编程（ASP）是用于建模和解决知识表示和推理问题的范式。有很多专门研究ASP（碎片）的硬度的结果。到目前为止，这些研究在计算复杂性以及以二分法式结果形式提出的细粒度见解方面取得了特征，当转化为其他形式主义（例如命题满意度）（SAT），甚至详细的参数化复杂性景观时，下界也会下降。源自图理论的参数化复杂性的通用参数是所谓的树宽，从某种意义上说，它捕获了程序的结构密度。最近，与SAT相关的基于树宽的求解器的数量有所增加。虽然有从（正常）ASP到SAT的翻译，但已知尚无保留树宽或至少跟踪树宽增加的减少。在本文中，我们提出了一种从正常ASP减少到SAT的新颖减少，它知道树宽，并确保略有增加的树宽是足够的。此外，我们展示了一个新的结果，该结果表明，在考虑树宽时，正常ASP的片段已经比SAT（在计算复杂性的合理假设下）要稍难。这也证实了我们的减少可能无法显着改善，并且不可避免地会略有增加树宽。最后，我们介绍了一项关于从正常ASP减少到SAT的新型减少的经验研究，在那里我们比较了通过已知的分解启发式方法获得的树宽度上限。总体而言，与现有翻译相比，我们的减少能力比这些启发式方法更好。
Answer Set Programming (ASP) is a paradigm for modeling and solving problems for knowledge representation and reasoning. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A generic parameter in parameterized complexity originating from graph theory is the so-called treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there are translations from (normal) ASP to SAT, no reduction that preserves treewidth or at least keeps track of the treewidth increase is known. In this paper we propose a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Further, we show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable. Finally, we present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decomposition heuristics. Overall, our reduction works better with these heuristics than existing translations.
