Skip to content

Quick Start Guide

This library collects tools for explaining why an ASP program is unsatisfiable. We build on top of the clingo API to offer preprocessing, subset computation, and constraint analysis helpers for building explanation systems. This repository is part of the Potassco suite.

Installation

Clingo-Explaid can easily be installed with pip:

pip install clingexplaid

Requirements : python >= 3.11 & clingo >= 5.7.1

Usage Example

Finding a single MUS

from clingexplaid.preprocessors import AssumptionPreprocessor, FilterSignature
from clingexplaid.unsat import SubsetComputer

PROGRAM = """
a(1..3).
{b(4..6)}.

a(X) :- b(X).

:- a(X), X>=3.
"""

ap = AssumptionPreprocessor(filters={FilterSignature("a", 1)})
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions)


def shrink_on_core(core) -> None:
    mus = sc.mus(core)
    print(mus)


ap.control.solve(assumptions=list(ap.assumptions), on_core=shrink_on_core)

The SubsetComputer.mus() method can simple be swapped with SubsetComputer.mss() or SubsetComputer.mcs() to compute the respective other subset types

Advanced Usage

Explore more ways to use clingexplaid