diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 25fd335..b03bc1e 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -1,40 +1,68 @@ -# Development +## Development -To improve code quality, we use [nox] to run linters, type checkers, unit -tests, documentation and more. We recommend installing nox using [pipx] to have -it available globally. +### Installation + +To install the project, run + +```bash +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: ```bash -# install python -m pip install pipx python -m pipx install nox - -# run all sessions nox +``` -# list all sessions -nox -l +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: -# run individual session -nox -s session_name +```bash +nox -s test +``` -# run individual session (reuse install) -nox -Rs session_name +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: + +```bash +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: + +```bash +nox -Rs format -- check +nox -Rs format ``` -Note that the nox sessions create [editable] installs. 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. +The former command allows you to inspect changes before applying them. -We also provide a [pre-commit][pre] config to autoformat code upon commits. It -can be set up using the following commands: +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][pre] config to automate this process. It can be +set up using the following commands: ```bash python -m pipx install pre-commit pre-commit install ``` +This blackens the source code whenever `git commit` is used. + [editable]: https://setuptools.pypa.io/en/latest/userguide/development_mode.html [nox]: https://nox.thea.codes/en/stable/index.html [pipx]: https://pypa.github.io/pipx/ diff --git a/LIMITATIONS.md b/LIMITATIONS.md new file mode 100644 index 0000000..7b13e9f --- /dev/null +++ b/LIMITATIONS.md @@ -0,0 +1,78 @@ +## 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](examples/misc/bad_mucs.lp): + +```MATLAB +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 provided `a(1)`, `a(2)`, `a(3)`, and `unsat` 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 diff --git a/README.md b/README.md index 2c1cc62..47d7c2a 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,24 @@ # clingexplaid +Tools to aid the development of explanation systems using clingo + +## Installation + +Clingo-Explaid easily be installed with `pip`: + +```bash +pip install clingexplaid +``` + +### Requirements + +- `python >= 3.9` +- `clingo >= 5.7.1` + +### Building from Source + +Please refer to [DEVELOPEMENT](DEVELOPMENT.md) + ## Usage Run the following for basic usage information: @@ -38,154 +57,28 @@ clingexplaid ### Examples -- A selection of examples can be found [here](examples) - -## Development - -### Installation - -To install the project, run +Given the simple program below [`simple.lp`](examples/misc/simple.lp) we want +to find the contained MUC (Minimal Unsatisfiable Core). -```bash -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: - -```bash -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: - -```bash -nox -s test ``` +a(1..5). +b(5..10). -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: - -```bash -nox -s dev -source .nox/dev/bin/activate +:- a(X), b(X). ``` -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: +For this we can call `clingexplaid` the following way: ```bash -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][pre] config to automate this process. It can be -set up using the following commands: - -```bash -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](examples/misc/bad_mucs.lp): - -```MATLAB -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 +clingexplaid examples/misc/simple.lp --muc 0 ``` -- 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: +This converts all facts of the program to choices and assumptions and returns +the contained MUC from that. ``` -NO MUCS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions -UNSATISFIABLE +MUC 1 +b(5) a(5) ``` -- 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 provided `a(1)`, `a(2)`, `a(3)`, and `unsat` 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 - -[black]: https://black.readthedocs.io/en/stable/ -[editable]: https://setuptools.pypa.io/en/latest/userguide/development_mode.html -[nox]: https://nox.thea.codes/en/stable/index.html -[pipx]: https://pypa.github.io/pipx/ -[pre]: https://pre-commit.com/ +A selection of more examples can be found [here](examples)