Computing Supported Models via Transformation to Stable Models
Fang Li, Gopal Gupta
TL;DR
<3-5 sentence high-level summary>The paper addresses the restriction imposed by stable-model minimality in Answer Set Programming and argues for the broader exploratory power of supported models. It introduces a polynomial-time transformation that converts any ground logic program into an auxiliary-program whose stable models correspond exactly to the original program's supported models, with correctness proofs and a Clingo-based implementation. The authors compare their ASP-based approach to Clark's Completion/SAT-based methods and demonstrate practical applications in software verification, medical diagnosis, and planning, highlighting the method's utility for non-minimal yet consistent reasoning. Overall, the work provides a practical, integrated tool for computing supported models within the ASP ecosystem, enabling richer exploratory reasoning beyond standard stable models.
Abstract
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.