Tools to aid the development of explanation systems using clingo
Project description
clingexplaid
Tools to aid the development of explanation systems using clingo
Installation
Clingo-Explaid easily be installed with pip
:
pip install clingexplaid
Requirements
python >= 3.9
clingo >= 5.7.1
Building from Source
Please refer to DEVELOPEMENT
Usage
Run the following for basic usage information:
clingexplaid -h
Interactive Mode
We provide an interactive terminal user interface (textual) where all modes are accessible in an interactive format. You can start this mode by using the command below.
clingexplaid <files> --interactive
Example: MUS Sudoku
Below is one Example call using our Sudoku Example.
clingexplaid examples/sudoku/encoding.lp examples/sudoku/instance.lp --interactive
Example: Show Decisions
This Example shows the interactive Solver Decision Tree generated from
examples/misc/sat_simple.lp
.
Clingo Application Class
The clingexplaid CLI (based on the clingo.Application
class) extends clingo
with <method>
and <options>
.
clingexplaid <method> <options>
<method>
: specifies which Clingexplaid method is used (Required)- Options:
--muc
:- Computes the Minimal Unsatisfiable Cores (MUCs) of the provided unsatisfiable program
--unsat-constraints
:- Computes the Unsatisfiable Constraints of the unsatisfiable program provided.
--show-decisions
:- Visualizes the decision process of clasp
- Options:
<options>
: Additional options for the different methods- For
--muc
:-a
,--assumption-signature
: limits which facts of the current program are converted to choices/assumptions for finding the MUCs (Default: all facts are converted)
- For
--show-decisions
:--decision-signature
: limits which decisions are shown in the visualization (Default: all atom's decisions are shown)
- For
Examples
Given the simple program below simple.lp
we want
to find the contained MUC (Minimal Unsatisfiable Core).
a(1..5).
b(5..10).
:- a(X), b(X).
For this we can call clingexplaid
the following way:
clingexplaid examples/misc/simple.lp --muc 0
This converts all facts of the program to choices and assumptions and returns the contained MUC from that.
MUC 1
b(5) a(5)
A selection of more examples can be found here
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for clingexplaid-1.0.14-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | aa0c3d0c087ab6386c7e504ff26e43cb7f1999f02086deb000164474f3fa2fbd |
|
MD5 | ced656a05d59fa5889e7b09a6be035aa |
|
BLAKE2b-256 | 51f45b924d8a56de27f624bcdf0bcbe455d3c4ed436a4fbc4bfc16e756e9d2b7 |