fixed README

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/

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

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 <filenames> <n> <method> <options>
 
 ### 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)