Witnesses for Answer Sets of Logic Programs

• Published in: ACM transactions on computational logic 2023-01, Vol.24 (2), p.1-46, Article 15
• Main Authors: Wang, Yisong, Eiter, Thomas, Zhang, Yuanlin, Lin, Fangzhen
• Format: Article
• Language: English
• Subjects: Artificial intelligence; Computing methodologies; Logic programming and answer set programming; Nonmonotonic, default reasoning and belief revision; Reasoning about belief and knowledge
• ISSN: 1529-3785; 1557-945X
• DOI: 10.1145/3568955

In this article, we consider Answer Set Programming (ASP). It is a declarative problem solving paradigm that can be used to encode a problem as a logic program whose answer sets correspond to the solutions of the problem. It has been widely applied in various domains in AI and beyond. Given that answer sets are supposed to yield solutions to the original problem, the question of “why a set of atoms is an answer set” becomes important for both semantics understanding and program debugging. It has been well investigated for normal logic programs. However, for the class of disjunctive logic programs, which is a substantial extension of that of normal logic programs, this question has not been addressed much. In this article, we propose a notion of reduct for disjunctive logic programs and show how it can provide answers to the aforementioned question. First, we show that for each answer set, its reduct provides a resolution proof for each atom in it. We then further consider minimal sets of rules that will be sufficient to provide resolution proofs for sets of atoms. Such sets of rules will be called witnesses and are the focus of this article. We study complexity issues of computing various witnesses and provide algorithms for computing them. In particular, we show that the problem is tractable for normal and headcycle-free disjunctive logic programs, but intractable for general disjunctive logic programs. We also conducted some experiments and found that for many well-known ASP and SAT benchmarks, computing a minimal witness for an atom of an answer set is often feasible.