# aspmc
(Algebraic) answer set counter based on a treewidth-aware cycle-breaking for normal answer set programs.
For usage on Linux you may also install this software as a pip package via
```
pip install aspmc
```
Documentation for usage as a python module is available [here](https://raki123.github.io/aspmc/).
Examples for command line usage are available below.
If you have any issues please contact us, or even better create an issue on GitHub.
For academic usage cite
* Eiter, T., Hecher, M., & Kiesel, R. (2021, September). Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (Vol. 18, No. 1, pp. 269-279).
## Development setup
For developement clone via
```
git clone --single-branch --branch=main git@github.com:raki123/aspmc.git
```
to avoid the download of the experimental results in branch `results`.
We include a setup bash script `setup.sh` that should automatically perform all steps below that are required to run our code. (Except for providing the c2d and miniC2D binary.)
### Python
* Python >= 3.6
All required modules are listed in `requirements.txt` and can be obtained by running
```
pip install -r requirements.txt
```
### Tree Decompositions via flow-cutter
We use [flow-cutter](https://github.com/kit-algo/flow-cutter-pace17) to obtain treedecompositions that are needed for our treedecomposition guided clark completion, obtaining treewidth upperbounds on the programs, variable order generation and more.
It is included as a git submodule.
The submodules can be obtained by running
```
git submodule update --init
```
flow-cutter further needs to be compiled via
```
cd aspmc/external/flow-cutter/
bash build.sh
```
### Knowledge Compilation via d4 or sharpSAT-TD
We use [d4](https://github.com/raki123/d4) or [sharpSAT-TD](https://github.com/raki123/sharpsat-td) for knowledge compilation. Note that both of these are forks of the original model counters [here](https://github.com/crillab/d4) and [here](https://github.com/Laakeri/sharpsat-td/), respectively. For d4 we added support for smooth compilation and for sharpSAT-TD we used the nicely thought out addition by Tuukka Korhonen and Matti Järvisalo to enable weighted model counting over semirings in that we added a custom semiring to compile an sd-DNNF.
Both are also included as a git submodules.
The submodules can be obtained by running
```
git submodule update --init
```
They can then be compiled via
```
cd aspmc/external/sharpsat-td/
mkdir bin
bash setupdev.sh
cd ../../../
cd aspmc/external/d4/
make -j4
cd ../../../
```
## Optionally: c2d and miniC2D
We also are able to use c2d to obtain d-DNNF representations.
The c2d binary can be provided under `aspmc/external/c2d/bin/` as `c2d_linux` and can be downloaded from [here](http://reasoning.cs.ucla.edu/c2d/).
The miniC2D binary (and the hgr2htree binary) can be provided under `aspmc/external/miniC2D/bin/linux/` as `miniC2D` (and `hgr2htree`) and can be downloaded from [here](http://reasoning.cs.ucla.edu/minic2d/).
Note that they are only available for research use.
## Usage
The basic usage is
```
aspmc: An Algebraic Answer Set Counter
aspmc version 1.1.1, Mar 22, 2024
python main.py [-m .] [-st .] [-c] [-s .] [-n] [-t] [-ds .] [-dt .] [-k .] [-g .] [-b .] [-v .] [-h] [<INPUT-FILES>]
--mode -m MODE set input mode to MODE:
* asp : take a normal answer set program as input (default)
* smodels : take a normal answer set program in smodels format as input
* optasp : take a normal answer set program with weak constraints as input
* cnf : take an (extended) cnf as input
* problog : take a problog program as input
* smproblog : take a problog program with negations as input
* meuproblog : take a problog program with extra decision and utility atoms as input
* mapproblog : take a problog program with extra evidence and map query atoms as input
* mpeproblog : take a problog program with extra evidence atoms as input
* dtpasp : take a probabilistic answer set program with extra decision and utility atoms as input
* credal : take a probabilistic answer set program with credal semantics as input
--strategy -st STRATEGY set solving strategy to STRATEGY:
* flexible : choose the solver flexibly
* compilation : use knowledge compilation (default)
--count -c not only output the equivalent cnf as out.cnf but also performs (algebraic) counting of the answer sets
--semiring -s SEMIRING use the semiring specified in the python file aspmc/semirings/SEMIRING.py
only useful with -m problog
--no_pp -n does not perform cycle breaking and outputs a normalized version of the input program as `out.lp`
the result is equivalent, ground and does not contain annotated disjunctions.
--treewidth -t print the treewidth of the resulting CNF
--decos -ds SOLVER set the solver that computes tree decompositions to SOLVER:
* flow-cutter : uses flow_cutter_pace17 (default)
--decot -dt SECONDS set the timeout for computing tree decompositions to SECONDS (default: 1)
--knowlege -k COMPILER set the knowledge compiler to COMPILER:
* sharpsat-td : uses a compilation version of sharpsat-td (default)
* sharpsat-td-live : uses a compilation version of sharpsat-td where compilation and counting are simultaneous
* d4 : uses the (slightly modified) d4 compiler.
* c2d : uses the c2d compiler.
* miniC2D : uses the miniC2D compiler.
--guide_clark -g GUIDE set the tree decomposition type to use to guide the clark completion to GUIDE:
* none : preform the normal clark completion without guidance
* ors : guide for or nodes only
* both : guide for both `and` and `or` nodes (default)
* adaptive : guide `both` that takes into account the cost of auxilliary variables
* choose : try to choose the best of the previous options bases on expected treewidth
--cycle-breaking -b STRATEGY set the cycle-breaking strategy to STRATEGY:
* none : do not perform cycle-breaking, not suitable for model counting
* tp : perform tp-unfolding, suitable for model counting (default)
* binary : use the strategy of Janhunen without local and global ranking constraints
not suitable for model counting
* binary-opt : use the strategy of Hecher, not suitable for model counting
* lt : use the strategy of Lin and Zhao, not suitable for model counting
* lt-opt : use a modified version of Lin and Zhao's strategy with a smaller encoding,
not suitable for model counting
--verbosity -v VERBOSITY set the logging level to VERBOSITY:
* debug : print everything
* info : print as usual
* result : only print results, warnings and errors
* warning : only print warnings and errors
* errors : only print errors
--help -h print this help and exit
```
### Examples
These examples are for when the code is downloaded via GitHub.
When using the pip package replace `python main.py` by `aspmc` to obtain the same result.
#### ASP example:
```
python main.py -m asp -c -f
a :- not b.
b :- not a.
```
Reads the program from stdin and counts its models.
```
python main.py -m asp -c -f test/test_cycle.lp
```
Reads the same program from file and counts its models.
#### problog example
```
python main.py -m problog -c -f
0.5::a.
b :- a.
query(b).
```
Evaluates the given simple program over the probability semiring.
```
python main.py -m problog -c -s maxplus -f
0.5::a.
b :- a.
query(b).
```
Evaluates the given simple program over the MaxPlus semiring.
Raw data
{
"_id": null,
"home_page": "https://github.com/raki123/aspmc",
"name": "aspmc",
"maintainer": null,
"docs_url": null,
"requires_python": "<4,>=3.6",
"maintainer_email": null,
"keywords": "probabilistic, model counting, logic programming, answer set programming",
"author": "R. Kiesel",
"author_email": "rafael.kiesel@tuwien.ac.at",
"download_url": "https://files.pythonhosted.org/packages/6d/35/091951987af0329634f16c15babc508b74280f580b9ea7d6da2f2b39ad4c/aspmc-1.1.1.tar.gz",
"platform": null,
"description": "# aspmc\n(Algebraic) answer set counter based on a treewidth-aware cycle-breaking for normal answer set programs.\n\nFor usage on Linux you may also install this software as a pip package via\n```\npip install aspmc\n```\nDocumentation for usage as a python module is available [here](https://raki123.github.io/aspmc/). \nExamples for command line usage are available below.\n\nIf you have any issues please contact us, or even better create an issue on GitHub.\n\nFor academic usage cite \n\n * Eiter, T., Hecher, M., & Kiesel, R. (2021, September). Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (Vol. 18, No. 1, pp. 269-279).\n\n## Development setup\nFor developement clone via \n```\ngit clone --single-branch --branch=main git@github.com:raki123/aspmc.git\n```\nto avoid the download of the experimental results in branch `results`.\n\nWe include a setup bash script `setup.sh` that should automatically perform all steps below that are required to run our code. (Except for providing the c2d and miniC2D binary.)\n\n### Python\n* Python >= 3.6\n\nAll required modules are listed in `requirements.txt` and can be obtained by running\n```\npip install -r requirements.txt\n```\n\n### Tree Decompositions via flow-cutter\nWe use [flow-cutter](https://github.com/kit-algo/flow-cutter-pace17) to obtain treedecompositions that are needed for our treedecomposition guided clark completion, obtaining treewidth upperbounds on the programs, variable order generation and more.\n\nIt is included as a git submodule.\n\nThe submodules can be obtained by running\n```\ngit submodule update --init\n```\n\nflow-cutter further needs to be compiled via\n```\ncd aspmc/external/flow-cutter/\nbash build.sh\n```\n\n\n### Knowledge Compilation via d4 or sharpSAT-TD \nWe use [d4](https://github.com/raki123/d4) or [sharpSAT-TD](https://github.com/raki123/sharpsat-td) for knowledge compilation. Note that both of these are forks of the original model counters [here](https://github.com/crillab/d4) and [here](https://github.com/Laakeri/sharpsat-td/), respectively. For d4 we added support for smooth compilation and for sharpSAT-TD we used the nicely thought out addition by Tuukka Korhonen and Matti J\u00e4rvisalo to enable weighted model counting over semirings in that we added a custom semiring to compile an sd-DNNF.\n\nBoth are also included as a git submodules.\n\nThe submodules can be obtained by running\n```\ngit submodule update --init\n```\n\nThey can then be compiled via \n```\ncd aspmc/external/sharpsat-td/\nmkdir bin\nbash setupdev.sh\ncd ../../../\ncd aspmc/external/d4/\nmake -j4\ncd ../../../\n```\n\n## Optionally: c2d and miniC2D\nWe also are able to use c2d to obtain d-DNNF representations. \nThe c2d binary can be provided under `aspmc/external/c2d/bin/` as `c2d_linux` and can be downloaded from [here](http://reasoning.cs.ucla.edu/c2d/).\nThe miniC2D binary (and the hgr2htree binary) can be provided under `aspmc/external/miniC2D/bin/linux/` as `miniC2D` (and `hgr2htree`) and can be downloaded from [here](http://reasoning.cs.ucla.edu/minic2d/).\n\nNote that they are only available for research use.\n\n## Usage\n\nThe basic usage is\n\n```\naspmc: An Algebraic Answer Set Counter\naspmc version 1.1.1, Mar 22, 2024\n\npython main.py [-m .] [-st .] [-c] [-s .] [-n] [-t] [-ds .] [-dt .] [-k .] [-g .] [-b .] [-v .] [-h] [<INPUT-FILES>]\n --mode -m MODE set input mode to MODE:\n * asp : take a normal answer set program as input (default)\n * smodels : take a normal answer set program in smodels format as input\n * optasp : take a normal answer set program with weak constraints as input\n * cnf : take an (extended) cnf as input\n * problog : take a problog program as input\n * smproblog : take a problog program with negations as input\n * meuproblog : take a problog program with extra decision and utility atoms as input\n * mapproblog : take a problog program with extra evidence and map query atoms as input\n * mpeproblog : take a problog program with extra evidence atoms as input\n * dtpasp : take a probabilistic answer set program with extra decision and utility atoms as input\n * credal : take a probabilistic answer set program with credal semantics as input\n --strategy -st STRATEGY set solving strategy to STRATEGY:\n * flexible : choose the solver flexibly \n * compilation : use knowledge compilation (default)\n --count -c not only output the equivalent cnf as out.cnf but also performs (algebraic) counting of the answer sets\n --semiring -s SEMIRING use the semiring specified in the python file aspmc/semirings/SEMIRING.py\n only useful with -m problog\n --no_pp -n does not perform cycle breaking and outputs a normalized version of the input program as `out.lp`\n the result is equivalent, ground and does not contain annotated disjunctions.\n --treewidth -t print the treewidth of the resulting CNF\n --decos -ds SOLVER set the solver that computes tree decompositions to SOLVER:\n * flow-cutter : uses flow_cutter_pace17 (default)\n --decot -dt SECONDS set the timeout for computing tree decompositions to SECONDS (default: 1)\n --knowlege -k COMPILER set the knowledge compiler to COMPILER:\n * sharpsat-td : uses a compilation version of sharpsat-td (default)\n * sharpsat-td-live : uses a compilation version of sharpsat-td where compilation and counting are simultaneous\n * d4 : uses the (slightly modified) d4 compiler. \n * c2d : uses the c2d compiler. \n * miniC2D : uses the miniC2D compiler. \n --guide_clark -g GUIDE set the tree decomposition type to use to guide the clark completion to GUIDE:\n * none : preform the normal clark completion without guidance\n * ors : guide for or nodes only \n * both : guide for both `and` and `or` nodes (default)\n * adaptive : guide `both` that takes into account the cost of auxilliary variables \n * choose : try to choose the best of the previous options bases on expected treewidth\n --cycle-breaking -b STRATEGY set the cycle-breaking strategy to STRATEGY:\n * none : do not perform cycle-breaking, not suitable for model counting\n * tp : perform tp-unfolding, suitable for model counting (default)\n * binary : use the strategy of Janhunen without local and global ranking constraints\n not suitable for model counting\n * binary-opt : use the strategy of Hecher, not suitable for model counting\n * lt : use the strategy of Lin and Zhao, not suitable for model counting\n * lt-opt : use a modified version of Lin and Zhao's strategy with a smaller encoding,\n not suitable for model counting\n --verbosity -v VERBOSITY set the logging level to VERBOSITY:\n * debug : print everything\n * info : print as usual\n * result : only print results, warnings and errors\n * warning : only print warnings and errors\n * errors : only print errors\n --help -h print this help and exit\n```\n\n### Examples\nThese examples are for when the code is downloaded via GitHub.\nWhen using the pip package replace `python main.py` by `aspmc` to obtain the same result.\n#### ASP example:\n```\npython main.py -m asp -c -f \na :- not b.\nb :- not a.\n```\nReads the program from stdin and counts its models.\n\n```\npython main.py -m asp -c -f test/test_cycle.lp\n```\nReads the same program from file and counts its models.\n\n#### problog example\n```\npython main.py -m problog -c -f\n0.5::a.\nb :- a.\nquery(b).\n```\nEvaluates the given simple program over the probability semiring.\n\n```\npython main.py -m problog -c -s maxplus -f\n0.5::a.\nb :- a.\nquery(b).\n```\nEvaluates the given simple program over the MaxPlus semiring.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "An efficient algebraic model counter.",
"version": "1.1.1",
"project_urls": {
"Homepage": "https://github.com/raki123/aspmc"
},
"split_keywords": [
"probabilistic",
" model counting",
" logic programming",
" answer set programming"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "febfe07fcd6b7a3ffd85e5d6d837389a6fa2acd1af55248e965ff7374a99fe77",
"md5": "a4d0a176c0bb07c9bd896e6e3a95fb13",
"sha256": "da87548d20c95ad8be01385e4abd944c9b64143d1a7a4e63e6c626f277b11dba"
},
"downloads": -1,
"filename": "aspmc-1.1.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "a4d0a176c0bb07c9bd896e6e3a95fb13",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<4,>=3.6",
"size": 16884005,
"upload_time": "2024-03-22T17:41:49",
"upload_time_iso_8601": "2024-03-22T17:41:49.595090Z",
"url": "https://files.pythonhosted.org/packages/fe/bf/e07fcd6b7a3ffd85e5d6d837389a6fa2acd1af55248e965ff7374a99fe77/aspmc-1.1.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "6d35091951987af0329634f16c15babc508b74280f580b9ea7d6da2f2b39ad4c",
"md5": "fdec35c8a33e342cc092928488714b9d",
"sha256": "1669e4a54ec3f6c7de2498438d09a2c2f4910a165c30167825aad59564ad04a4"
},
"downloads": -1,
"filename": "aspmc-1.1.1.tar.gz",
"has_sig": false,
"md5_digest": "fdec35c8a33e342cc092928488714b9d",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<4,>=3.6",
"size": 16685727,
"upload_time": "2024-03-22T17:41:53",
"upload_time_iso_8601": "2024-03-22T17:41:53.156599Z",
"url": "https://files.pythonhosted.org/packages/6d/35/091951987af0329634f16c15babc508b74280f580b9ea7d6da2f2b39ad4c/aspmc-1.1.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-03-22 17:41:53",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "raki123",
"github_project": "aspmc",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"requirements": [],
"lcname": "aspmc"
}
JSON
