Merge pull request #3 from krr-up/hannes

Preparation for Beta Release 0.1

.github/workflows/ci-test.yml

@@ -23,16 +23,21 @@ jobs:
     - name: "checkout repository"
       uses: actions/checkout@v3
 
-    - name: "setup python 3.7"
+    - name: "setup python 3.9"
       uses: actions/setup-python@v4
       with:
-        python-version: 3.7
+        python-version: 3.9
 
     - name: "setup python 3.11"
       uses: actions/setup-python@v4
       with:
         python-version: 3.11
-
+
+    - name: "setup python 3.12"
+      uses: actions/setup-python@v4
+      with:
+        python-version: 3.12
+
     - name: install nox
       run: python -m pip install nox
 

.gitignore

@@ -20,12 +20,12 @@ pip-delete-this-directory.txt
 # Unit test / coverage reports
 .pytest_cache/
 
+#venv
+.venv
+
 # pyenv
 .python-version
 
-# venv
-.venv
-
 # mypy
 .mypy_cache/
 .dmypy.json

.pre-commit-config.yaml

@@ -1,27 +1,35 @@
 repos:
   - repo: https://github.com/myint/autoflake
-    rev: v1.4
+    rev: v2.3.0
     hooks:
     - id: autoflake
       args: ["--in-place",  "--imports=clingexplaid", "--ignore-init-module-imports", "--remove-unused-variables"]
       exclude: ^.github/
 
   - repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v4.3.0
+    rev: v4.5.0
     hooks:
     - id: end-of-file-fixer
     - id: trailing-whitespace
       exclude: ^.github/
 
   - repo: https://github.com/pycqa/isort
-    rev: 5.11.5
+    rev: 5.13.2
     hooks:
       - id: isort
-        args: ["--profile", "black"]
         exclude: ^.github/
 
   - repo: https://github.com/psf/black
-    rev: 22.3.0
+    rev: 24.2.0
     hooks:
     - id: black
       exclude: ^.github/
+
+  - repo: https://github.com/executablebooks/mdformat
+    rev: 0.7.17
+    hooks:
+    - id: mdformat
+      args: ["--wrap", "79"]
+      exclude: ^doc/
+      additional_dependencies:
+      - mdformat-gfm

CHANGES.md

@@ -0,0 +1,5 @@
+# Changes
+
+## v0.1.0
+
+- create project

CONTRIBUTING.md

@@ -0,0 +1,31 @@
+# Contributing
+
+Thanks for considering a contribution to clingexplaid. ❤️
+
+## How to get help or discuss possible contributions
+
+To avoid duplicating issues, please search our [issue tracker][issues] and our
+[mailing list][mailing_list] before filing a new issue.
+
+- Open an [issue][new_issue] describing your problem.
+- [Subscribe] to our mailing list on SourceForge.
+
+## How to make a contribution
+
+- Fork the [clingexplaid][project_url] repository and create a branch for your
+  changes.
+- Submit a pull request to the master branch with your changes.
+- Respond to feedback on your pull request.
+- If everything is fine your pull request is merged. 🥳
+
+## License
+
+When contributing to this project, you agree that you have authored 100% of the
+content, that you have the necessary rights to the content and that the content
+you contribute may be provided under the project license.
+
+[issues]: https://github.com/krr-up/clingo-explaidissues/
+[mailing_list]: https://sourceforge.net/p/potassco/mailman/potassco-users/
+[new_issue]: https://github.com/krr-up/clingo-explaidissues/new/
+[project_url]: https://github.com/krr-up/clingo-explaid
+[subscribe]: https://sourceforge.net/projects/potassco/lists/potassco-users/

DEPLOYMENT.md

@@ -0,0 +1,15 @@
+# Deployment
+
+Releases are deployed on [pypi] whenever a tag of form `vMajor.Minor.Revision`
+is pushed. Furthermore, the deployment workflow can be triggered manually to
+deploy test releases on [test.pypi].
+
+For this to work, the workflow has to be granted permission to deploy on the
+two services. Please follow this packaging [guide] to setup your accounts
+accordingly. We also recommend to setup a github [environment] to restrict
+which contributors can deploy packages.
+
+[environment]: https://docs.github.com/en/actions/deployment/targeting-different-environments/using-environments-for-deployment/
+[guide]: https://packaging.python.org/en/latest/guides/publishing-package-distribution-releases-using-github-actions-ci-cd-workflows/
+[pypi]: https://pypi.org/
+[test.pypi]: https://test.pypi.org/

DEVELOPMENT.md

@@ -0,0 +1,41 @@
+# 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.
+
+```bash
+# install
+python -m pip install pipx
+python -m pipx install nox
+
+# run all sessions
+nox
+
+# list all sessions
+nox -l
+
+# run individual session
+nox -s session_name
+
+# run individual session (reuse install)
+nox -Rs session_name
+```
+
+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.
+
+We also provide a [pre-commit][pre] config to autoformat code upon commits. It
+can be set up using the following commands:
+
+```bash
+python -m pipx install pre-commit
+pre-commit install
+```
+
+[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/

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2021 Susana Hahn
+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

README.md

@@ -1,35 +1,52 @@
 # clingexplaid
 
-This project template is configured to ease collaboration. Linters, formatters,
-and actions are already configured and ready to use.
-
-To use the project template, run the `init.py` script to give the project a
-name and some metadata. The script can then be removed afterward and the
-`setup.cfg` file adjusted.
-
-## Installation
-
-```shell
-pip install clingexplaid
-```
-
 ## Usage
 
-```shell
+Run the following for basic usage information:
+
+```bash
 clingexplaid -h
 ```
 
-Compute Minimal Unsatisfiable Core from unsatisfiable program:
+The clingexplaid CLI (based on the `clingo.Application` class) can  be called using this generic command.
 
-```shell
-clingexplaid <filenames> --assumption-signature signature/arity
+```bash
+clingexplaid <filenames> <n> <method> <options>
 ```
 
-+ `--assumption-signature` is optional to allow for only specific facts to be transformed to assumptions
-	+ if no such option is given all facts are transformed to assumptions regardless of their signature
++ `<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:
@@ -85,6 +102,79 @@ 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
+
+
 [doc]: https://potassco.org/clingo/python-api/current/
 [nox]: https://nox.thea.codes/en/stable/index.html
 [pipx]: https://pypa.github.io/pipx/