Computing Supported Models via Transformation to Stable Models

This project implements a system for computing supported models of logic programs using standard Answer Set Programming (ASP) solvers. Supported models, introduced by Apt, Blair, and Walker (1988), offer a semantics for logic programs that relaxes the minimality constraint of stable models while maintaining logical consistency through a support condition.

Supported Models

A supported model is an interpretation where:

1. All rules are satisfied (it is a model of the program)
2. Every true atom is supported by some rule whose body is satisfied

This allows for non-minimal but logically consistent models that can capture cyclic dependencies and provide valuable exploratory reasoning capabilities. While every stable model is a supported model, the converse does not hold—supported models can include self-supporting cycles that stable models would exclude.

Transformation Approach

The solver enables computation of supported models using standard stable model solvers like Clingo through a polynomial-time ASP-to-ASP transformation. The key idea is to decouple conjunctive rule bodies using auxiliary atoms that represent when the body is disabled (does not hold).

For a rule of the form H :- L1, L2, ..., Ln., the transformation introduces an auxiliary atom _dm_X__ that captures when the body fails. Using De Morgan's law, the rule is transformed into:

• H :- not _dm_X__. (head is true if body is not disabled)
• _dm_X__ :- not L1. (auxiliary true if positive literal L1 is false)
• _dm_X__ :- L_i. (auxiliary true if negative literal not B is present and B is true)
• ... for each literal in the original body

The stable models of the transformed program correspond exactly to the supported models of the original program, enabling direct use of existing ASP solvers without requiring external SAT solvers or completion-based transformations.

Solver Usage

The solver consists of a Python script (consistency_solver.py) that performs the transformation and relies on the Clingo ASP solver to find the models of the transformed program.

Prerequisites

• Python 3
• Clingo (Answer Set Programming solver) - Make sure clingo is installed and accessible in your system's PATH.

Steps

1. Save your ASP program in a file (e.g., my_program.lp).
2. Run the transformation script, piping the output to a new file:

   python consistency_solver.py my_program.lp > transformed_program.lp

3. Solve the transformed program using Clingo to find the supported models:

   clingo transformed_program.lp --models=0

   The --models=0 option instructs Clingo to find all stable models of the transformed program, which correspond to the supported models of the original.

Example

Consider the following ASP program with cyclic dependencies (test_program.lp):

p :- q, not r.
q :- p.
:- r. % Constraint: r must be false

This program has cyclic dependencies involving negation. Under stable model semantics, only the empty model satisfies this program. However, under supported model semantics, there is an additional supported model.

Using the supported models transformation:

1. Transform the program:

   python consistency_solver.py test_program.lp > transformed_program.lp

   The transformed_program.lp contains auxiliary atoms (prefixed by _dm_) that capture when rule bodies are disabled.

2. Solve with Clingo:

   clingo transformed_program.lp --models=0

Expected Output:

Answer: 1
_dm_0 _dm_1

Answer: 2
p q

SATISFIABLE

Models       : 2
Calls        : 1

The first model is the minimal (empty) model. The second model {p, q} is a supported model but not a stable model—it represents a self-supporting cycle where each atom is justified by the program's rules, demonstrating the key advantage of supported models for exploratory reasoning.