Metadata-Version: 2.1
Name: clingexplaid
Version: 1.0.9
Summary: A template project.
Author-email: Hannes Weichelt <hweichelt@uni-potsdam.de>
License: MIT License
        
        Copyright (c) 2024 Hannes Weichelt
        
        Permission is hereby granted, free of charge, to any person obtaining a copy
        of this software and associated documentation files (the "Software"), to deal
        in the Software without restriction, including without limitation the rights
        to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
        copies of the Software, and to permit persons to whom the Software is
        furnished to do so, subject to the following conditions:
        
        The above copyright notice and this permission notice shall be included in all
        copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
        FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
        AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
        LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
        OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
        SOFTWARE.
        
Project-URL: Homepage, https://github.com/krr-up/clingo-explaid
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: clingo>=5.7.1
Requires-Dist: autoflake
Provides-Extra: format
Requires-Dist: black; extra == "format"
Requires-Dist: isort; extra == "format"
Requires-Dist: autoflake; extra == "format"
Provides-Extra: lint-pylint
Requires-Dist: pylint; extra == "lint-pylint"
Provides-Extra: typecheck
Requires-Dist: types-setuptools; extra == "typecheck"
Requires-Dist: mypy; extra == "typecheck"
Provides-Extra: test
Requires-Dist: coverage[toml]; extra == "test"
Provides-Extra: doc
Requires-Dist: sphinx; extra == "doc"
Requires-Dist: furo; extra == "doc"
Requires-Dist: nbsphinx; extra == "doc"
Requires-Dist: sphinx_copybutton; extra == "doc"
Requires-Dist: myst-parser; extra == "doc"
Provides-Extra: dev
Requires-Dist: clingexplaid[lint_pylint,test,typecheck]; extra == "dev"

# clingexplaid

## Usage

Run the following for basic usage information:

```bash
clingexplaid -h
```

The clingexplaid CLI (based on the `clingo.Application` class) can be called
using this generic command.

```bash
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>`: 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)

### Examples

- A selection of examples can be found [here](examples)

## Development

### 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
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
```

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
```

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
```

- 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

[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/
