A template project.
Project description
clingexplaid
Usage
Run the following for basic usage information:
clingexplaid -h
The clingexplaid CLI (based on the clingo.Application
class) can be called
using this generic command.
clingexplaid <filenames> <n> <method> <options>
<filenames>
: has to be replaced by a list of all files or a single filename<n>
: defines how many models are computed (Default=1
, All=0
)<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
- A selection of examples can be found here
Development
Installation
To install the project, run
pip install .
To improve code quality, we run linters, type checkers, and unit tests. The tools can be run using nox. We recommend installing nox using pipx to have it available globally:
python -m pip install pipx
python -m pipx install nox
nox
You can invoke nox -s
to run individual sessions. For example, to install
your package into a virtual environment and run your test suite, invoke:
nox -s test
We also provide a nox session that creates an environment for development. The project is installed in editable mode into this environment along with linting, type checking and formatting tools. Activating it allows your editor of choice to access these tools for, e.g., linting and autocompletion. To create and then activate virtual environment run:
nox -s dev
source .nox/dev/bin/activate
Furthermore, we provide individual sessions to easily run linting, type
checking and formatting via nox. These also create editable installs. So you
can safely skip the recreation of the virtual environment and reinstallation of
your package in subsequent runs by passing the -R
command line argument. For
example, to auto-format your code using black, run:
nox -Rs format -- check
nox -Rs format
The former command allows you to inspect changes before applying them.
Note that editable installs have some caveats. In case there are issues, try
recreating environments by dropping the -R
option. If your project is
incompatible with editable installs, adjust the noxfile.py
to disable them.
We also provide a pre-commit config to automate this process. It can be set up using the following commands:
python -m pipx install pre-commit
pre-commit install
This blackens the source code whenever git commit
is used.
Problems and Limitations
Meta-encoding based approach (ASP-Approach)
Important Notes:
- The Meta-encoding approach as it stands is not fully functional
Problem:
- In the meta encoding all facts (or a selection matching a certain signature) are transformed into assumptions which are then used as the assumption set for finding the MUC
- During the MUC search when subsets of this assumption set are fixed for satisfiability checking it is important that even though they are not fixed, the other assumptions are not assumed as false but as undefined
- This is currently not possible with the meta-encoding, since assumptions are chosen through a choice rule and all assumptions that aren't selected are defaulted to false
- This doesn't allow for properly checking if such subsets entail unsatisfiability and thus prevents us from finding the proper MUCs
Specifying Assumption Set using only Signatures
Important Notes:
- clingo-explaid provides the
--muc
mode which gives you Minimal Unsatisfiable Cores for a given set of assumption signatures that can be defined with-a
- These signatures though allow not always for finding the best fitting MUC for a given encoding, compared to an assumption set generated by hand
Problem:
- Imagine this example encoding:
a(1..3).
:- a(X).
unsat.
:- unsat.
- So when I execute
clingexplaid examples/misc/bad_mucs.lp --muc 0
I get the MUCs:
MUC 1
a(3)
MUC 2
a(2)
MUC 3
a(1)
MUC 4
unsat
- So you would generally expect that executing
clingexplaid examples/misc/bad_mucs.lp --muc 0 -a/1
would return the first 3 found MUCs from before - But what actually happens is that there are no MUCs detected:
NO MUCS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions
UNSATISFIABLE
- This is actually due to an implicit
(unsat, False)
in the first 3 MUCs that isn't printed - Since the standard mode of
--muc
converts all facts to choices when no-a
is provideda(1)
,a(2)
,a(3)
, andunsat
are all converted to choices - We know that for the program to become satisfiable
unsat
cannot be true (line 4) - But since it is provided as a fact the choice rule conversion is necessary for the iterative deletion algorithm to find any MUCs
- This holds vice versa for the last MUC 4 just so that all
a/1
need to be converted to choice rules for the MUC to be found
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.9-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 2f703a8a8c19207ca1d0e3554ef69c90bbe90d07b80f4f335c315b5ea4acdfd6 |
|
MD5 | c8c800653d05afc28d18224b90fca6d8 |
|
BLAKE2b-256 | fe76aa3bf384a70f07996adfd6bbe57f560fde668bfa0de4d0d10fc291a11343 |