A simple proof-theoretic characterization of stable models: Reduction to difference logic and experiments

作     者：Gebser, Martin Giunchiglia, Enrico Maratea, Marco Mochi, Marco 

作者机构：Univ Klagenfurt AICS Klagenfurt Austria Univ Genoa DIBRIS Genoa Italy Univ Calabria DEMACS Arcavacata Di Rende Italy 

出 版 物：《ARTIFICIAL INTELLIGENCE》 (Artif Intell)

年 卷 期：2025年第340卷

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Logic programming Stable models Answer set programming Difference logic 

摘      要：Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model- theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver YICES, to the translation- based ASP solver LP2DIEE and to CLIvGo on domains from the Basic Decision track of the 2017 Answer Set Programming competition. The results show that our approach is competitive to and often better than LP2DIEE, and that it can also be faster than CLIvGo on non-tight domains.