论文标题
LP2PB：将答案集转换为伪树立理论
LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
论文作者
论文摘要
答案集编程（ASP）是一个完善的知识代表形式主义。大多数ASP求解器都是基于布尔可满足性解决方案的技术（扩展）。尽管这些求解器在许多实际应用中都非常成功，但它们的强度受其基本证明系统（分辨率）的限制。在本文中，我们提出了一种新的工具LP2PB，该工具将ASP程序转化为伪树状理论，该理论基于（更强的）切割平面系统的求解器。我们评估了我们的工具，以及针对传统ASP基准测试的ASP以及伪树生解决方案的基准测试的潜力。我们的结果是混合的：总的来说，传统的ASP求解器仍然优于我们的翻译方法，但是在以相反的方式发生平衡的情况下，确定了几个基准家族，从而表明进一步调查对ASP的更强大的证明系统是有价值的。
Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable.
