In answer set programming (ASP), answer sets capture solutions to search problems of interest and thus the efficient computation of answer sets is of utmost importance. One viable implementation strategy is provided by translation-based ASP where logic programs are translated into other KR formalisms such as Boolean satisfiability (SAT), SAT modulo theories (SMT), and mixed-integer programming (MIP). Consequently, existing solvers can be harnessed for the computation of answer sets. Many of the existing translations rely on program completion and level rankings to capture the minimality of answer sets and default negation properly. In this work, we take level ranking constraints into reconsideration, aiming at their generalizations to cover aggregate-based extensions of ASP in more systematic way. By applying a number of program transformations, ranking constraints can be rewritten in a general form that preserves the structure of monotone and convex aggregates and thus offers a uniform basis for their incorporation into translation-based ASP. The results open up new possibilities for the implementation of translators and solver pipelines in practice.
翻译:在回答集编程(ASP)中,回答集捕获了相关搜索问题的解,因此高效计算回答集至关重要。一种可行的实现策略是基于翻译的ASP,其中逻辑程序被翻译成其他知识表示形式,如布尔可满足性(SAT)、SAT模理论(SMT)和混合整数规划(MIP)。由此,可利用现有求解器进行计算回答集。许多现有翻译依赖于程序完备化与层级排序来正确捕捉回答集的最小性和缺省否定。本文重新审视层级排序约束,旨在将其推广至更系统地覆盖基于聚合的ASP扩展。通过应用一系列程序变换,排序约束可重写为保留单调与凸聚合结构的通用形式,从而为其融入基于翻译的ASP提供统一基础。这些结果为实践中翻译器与求解器流程的实现开辟了新可能性。