Skip to content

clingexplaid

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.

Unsatisfiable programs in Answer Set Programming (ASP) can be challenging to debug or explain. clingexplaid helps you find you to identify the core of that unsatisfiability, so you can debug encodings, explain results to users, or build interactive explanation tools on top of clingo.

  • Getting Started

    Install clingexplaid and compute your first unsatisfiable subset in a few lines of Python.

    Quick Start Guide

  • Examples

    Practical examples for subsets, unsatisfiable constraints, pre-processors and transformers.

    See Examples

  • Reference

    Detailed API documentation of all modules, classes and functions.

    API Documentation

What's inside

clingexplaid is structured as a set of building blocks that can be combined freely:

  • Pre-processors turn selected facts of a program into assumptions. This is the necessary first step for every subset computation, since the solver can only reason about which assumptions cause a conflict. See clingexplaid.preprocessors.

  • Subset computation finds the relevant subsets of an unsatisfiable assumption set: Minimal Unsatisfiable Subsets (MUS), Maximal Satisfiable Subsets (MSS) and Minimal Correction Sets (MCS), either a single one or enumerated one after the other. See clingexplaid.unsat.

  • Unsatisfiable constraints identifies which integrity constraints of a program are violated and therefore responsible for unsatisfiability. See the Unsatisfiable Constraints examples.

  • Transformers rewrite the abstract syntax tree of a program, for example to tag rules with identifiers, relax constraints or remove optimization statements. See clingexplaid.transformers.

  • Propagators hook into the solving process and record the order in which the solver makes its decisions, which helps to trace how a conflict arises. See clingexplaid.propagators.

A first look

Finding multiple MUSs

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

PROGRAM = """
a(1..3).
b(1..3).

:- a(X), b(X).
"""

ap = AssumptionPreprocessor()
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions)

for i, mus in enumerate(sc.multiple()):
    print(f"{i}:", mus)

Every fact of the program is turned into an assumption, and the SubsetComputer then enumerates all minimal sets of facts that cannot hold together. Head over to the Quick Start Guide for a step-by-step introduction.

Info

clingexplaid is part of the Potassco suite.