Answer Set Programming (ASP) with stable model semantics has proven highly effective for knowledge representation and reasoning. However, the minimality requirement of stable models can be restrictive for applications requiring exploration of non-minimal but logically consistent solution spaces. Supported models, introduced by Apt, Blair, and Walker in 1988, relax this minimality constraint while maintaining a support condition ensuring every true atom is justified by some rule. Despite their theoretical significance, supported models lack practical computational tools integrated with modern ASP solvers. We present a novel transformation-based method enabling computation of supported models using standard ASP infrastructure. Our approach transforms any ground logic program into an equivalent program whose stable models correspond exactly to the supported models of the original program. We implement this transformation for Clingo, providing the first practical tool for computing supported models with state-of-the-art ASP solvers. We demonstrate applications in software verification, medical diagnosis, and planning where supported models enable valuable exploratory reasoning capabilities beyond those provided by stable models. We also provide an empirical evaluation to justify the practical utility of our approach compared to established methods. Our implementation is publicly available and compatible with standard ASP syntax.
翻译:具有稳定模型语义的答案集编程(ASP)已被证明在知识表示与推理方面极为有效。然而,稳定模型的最小性要求对于需要探索非最小但逻辑一致的解空间的应用可能构成限制。Apt、Blair和Walker于1988年提出的支持模型放宽了这一最小性约束,同时保留了支持条件,确保每个真原子均由某个规则所证明。尽管具有理论意义,支持模型缺乏与现代ASP求解器集成的实用计算工具。本文提出一种基于转换的新方法,能够利用标准ASP基础设施计算支持模型。我们的方法将任意基础逻辑程序转换为一个等价程序,其稳定模型与原程序的支持模型精确对应。我们为Clingo实现了该转换,提供了首个利用先进ASP求解器计算支持模型的实用工具。我们展示了支持模型在软件验证、医疗诊断和规划中的应用,这些领域需要超越稳定模型所提供的探索性推理能力。我们还提供了实证评估,以证明本方法相较于现有方法的实用价值。我们的实现已公开提供,并与标准ASP语法兼容。