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.
翻译:稳定模型语义下的答案集程序设计在知识表示与推理领域已展现出卓越效能。然而,对于需要探索非最小但逻辑一致的解空间的应用场景,稳定模型的最小性要求可能构成限制。Apt、Blair 和 Walker 于 1988 年提出的支持模型放宽了该最小性约束,同时保留了支持条件以确保每个真原子都能被某个规则所验证。尽管具有理论重要性,支持模型目前仍缺乏与现代 ASP 求解器集成的实用计算工具。本文提出一种基于转换的新方法,能够利用标准 ASP 基础设施计算支持模型。该方法将任意基础逻辑程序转换为等价程序,使得转换后程序的稳定模型恰好对应原程序的支持模型。我们为 Clingo 实现了该转换,首次提供了利用前沿 ASP 求解器计算支持模型的实用工具。我们展示了支持模型在软件验证、医疗诊断和规划领域的应用案例,这些案例中支持模型能够实现超越稳定模型的探索性推理能力。我们还通过实证评估验证了本方法相较于现有方案的实用价值。我们的实现已公开提供,并兼容标准 ASP 语法。