声明式编程中的命题可满足性

回答集编程（ASP）范式是使用逻辑解决搜索问题的一种方式。给定一个搜索问题，要解决它，人们设计一个逻辑理论，使得该理论的模型代表问题的解。要计算问题的解，需要计算相应理论的模型。已经基于具有稳定模型语义的逻辑编程开发了几种回答集编程形式。在本文中，我们表明谓词演算的逻辑也产生了 ASP 范式的有效实现，其精神类似于具有稳定模型语义的逻辑编程，并且具有相似的应用范围。具体来说，我们提出了两种基于谓词演算的逻辑作为编码搜索问题的形式。我们表明这些逻辑的表达能力由 NP-search 类给出。我们演示了如何在编程中使用它们，并开发了用于模型查找的计算工具。对于其中一种逻辑，我们的技术将问题简化为命题可满足性问题，并允许使用现成的可满足性求解器。另一种逻辑的语言具有更复杂的语法，并提供显式的方法来建模一些高级约束。对于这种逻辑中的理论，我们设计了自己的求解器，利用扩展的语法。我们展示了实验结果，证明了整体方法的计算有效性。