# Bauhaus
`bauhaus` is a Python package for spinning up propositional logic encodings from object-oriented Python code.
## Features
- Create propositional variables from Python classes
- Build naive SAT encoding constraints from propositional variables
- At most one
- At least one
- Exactly one
- At most K
- Implies all
- Compile constraints into a theory in conjunctive or negation normal form
- With `python-nnf`, submit a theory to a SAT solver
- Theory introspection
## Installation
Install `bauhaus` by running
```bash
pip install bauhaus
```
## How is it used?
Create Encoding objects that you intend to compile to an SAT. Encoding objects will store your model's propositional variables and constraints on the fly.
```python
from bauhaus import Encoding, proposition, constraint
e = Encoding()
```
Create propositional variables by decorating class definitions with `@proposition`.
```python
@proposition(e) # Each instance of A is stored as a proposition
class A(object): pass
```
Create constraints by decorating classes, methods, or invoking the constraint methods.
```python
# Each instance of A implies the right side
@constraint.implies_all(e, right=['hello'])
# At most two of the A instances are true
@constraint.at_most_k(e, 2)
@proposition(e)
class A(object):
def __init__(self, val):
self.val = val
def __repr__(self):
return f"A.{self.val}"
# Each instance of A implies the result of the method
@constraint.implies_all(e)
def method(self):
return self.val
# At most one of the inputs is true.
constraint.add_at_most_one(e, A, A.method, Var('B'))
```
Compile your theory into conjunctive or negation normal form (note: the theory is truncated),
```python
objects = [A(val) for val in range(1,4)]
theory = e.compile()
>> And({And({Or({Var(3), ~Var(A.3)}), Or({Var(1), ~Var(A.1)}),
...
And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})})
```
And view the origin of each constraint, from the propositional object to the final constraint.
(Note: the introspection is truncated)
```python
e.introspect()
>>
constraint.at_most_k: function = A k = 2:
(~Var(A.3), ~Var(A.1)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})
(~Var(A.3), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})
(~Var(A.1), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})
Final at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})
...
...
```
## Contribute
Head over to our [code of conduct](CODE_OF_CONDUCT.md) and get a feel for the
library by reading our [architecture design](https://bauhaus.readthedocs.io/en/latest/architecture.html)
and [documentation](https://bauhaus.readthedocs.io/en/latest/index.html).
- Issue Tracker: https://github.com/QuMuLab/bauhaus/issues
- Source Code: https://github.com/QuMuLab/bauhaus
- Join us! http://mulab.ai/
## Support
If you are having issues, please let us know.
Reach out to us at karishma.daga@queensu.ca or by creating a GitHub issue.
## License
The project is licensed under the MIT license for the Queen's Mu Lab
### Citing This Work
`bauhaus` was created by Karishma Daga under mentorship of Christian Muise at Queen's University, Kingston.
Raw data
{
"_id": null,
"home_page": "",
"name": "bauhaus",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.4",
"maintainer_email": "",
"keywords": "logic nnf sat constraints encodings",
"author": "Karishma Daga, Christian Muise",
"author_email": "karishma.daga@queensu.ca, christian.muise@queensu.ca",
"download_url": "https://files.pythonhosted.org/packages/f9/71/862964f0ac099f8e4b92d1b930786c8a76d27a9115c6361ce6de558973b4/bauhaus-1.1.4.tar.gz",
"platform": null,
"description": "# Bauhaus\n`bauhaus` is a Python package for spinning up propositional logic encodings from object-oriented Python code.\n\n## Features\n- Create propositional variables from Python classes\n- Build naive SAT encoding constraints from propositional variables\n - At most one\n - At least one\n - Exactly one\n - At most K\n - Implies all\n- Compile constraints into a theory in conjunctive or negation normal form\n- With `python-nnf`, submit a theory to a SAT solver\n- Theory introspection\n\n## Installation\n\nInstall `bauhaus` by running\n\n```bash\npip install bauhaus\n```\n\n## How is it used?\n\nCreate Encoding objects that you intend to compile to an SAT. Encoding objects will store your model's propositional variables and constraints on the fly.\n\n```python\nfrom bauhaus import Encoding, proposition, constraint\ne = Encoding()\n```\n\nCreate propositional variables by decorating class definitions with `@proposition`.\n\n```python\n@proposition(e) # Each instance of A is stored as a proposition\nclass A(object): pass\n```\n\nCreate constraints by decorating classes, methods, or invoking the constraint methods.\n\n```python\n# Each instance of A implies the right side\n@constraint.implies_all(e, right=['hello'])\n# At most two of the A instances are true\n@constraint.at_most_k(e, 2)\n@proposition(e)\nclass A(object):\n\n def __init__(self, val):\n self.val = val\n\n def __repr__(self):\n return f\"A.{self.val}\"\n\n # Each instance of A implies the result of the method\n @constraint.implies_all(e)\n def method(self):\n return self.val\n\n# At most one of the inputs is true.\nconstraint.add_at_most_one(e, A, A.method, Var('B'))\n```\n\nCompile your theory into conjunctive or negation normal form (note: the theory is truncated),\n\n```python\nobjects = [A(val) for val in range(1,4)]\ntheory = e.compile()\n>> And({And({Or({Var(3), ~Var(A.3)}), Or({Var(1), ~Var(A.1)}),\n ...\n And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})})\n```\n\nAnd view the origin of each constraint, from the propositional object to the final constraint.\n(Note: the introspection is truncated)\n\n```python\ne.introspect()\n>>\nconstraint.at_most_k: function = A k = 2:\n\n(~Var(A.3), ~Var(A.1)) =>\nOr({~Var(A.1), ~Var(A.2), ~Var(A.3)})\n\n\n(~Var(A.3), ~Var(A.2)) =>\nOr({~Var(A.1), ~Var(A.2), ~Var(A.3)})\n\n\n(~Var(A.1), ~Var(A.2)) =>\nOr({~Var(A.1), ~Var(A.2), ~Var(A.3)})\n\n\nFinal at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})\n...\n...\n```\n\n## Contribute\nHead over to our [code of conduct](CODE_OF_CONDUCT.md) and get a feel for the\nlibrary by reading our [architecture design](https://bauhaus.readthedocs.io/en/latest/architecture.html)\nand [documentation](https://bauhaus.readthedocs.io/en/latest/index.html).\n- Issue Tracker: https://github.com/QuMuLab/bauhaus/issues\n- Source Code: https://github.com/QuMuLab/bauhaus\n- Join us! http://mulab.ai/\n\n## Support\nIf you are having issues, please let us know.\nReach out to us at karishma.daga@queensu.ca or by creating a GitHub issue.\n\n## License\nThe project is licensed under the MIT license for the Queen's Mu Lab\n\n### Citing This Work\n`bauhaus` was created by Karishma Daga under mentorship of Christian Muise at Queen's University, Kingston.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Build logical theories for SAT solvers on the fly",
"version": "1.1.4",
"split_keywords": [
"logic",
"nnf",
"sat",
"constraints",
"encodings"
],
"urls": [
{
"comment_text": "",
"digests": {
"md5": "2034050226226dd99b2b50f87004cd0d",
"sha256": "cbfe31126f65bd143d3d7e5a6ae318b20d0a782fd8cf26173baf36504a3e98a1"
},
"downloads": -1,
"filename": "bauhaus-1.1.4-py3-none-any.whl",
"has_sig": false,
"md5_digest": "2034050226226dd99b2b50f87004cd0d",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.4",
"size": 16676,
"upload_time": "2022-12-13T05:05:21",
"upload_time_iso_8601": "2022-12-13T05:05:21.193086Z",
"url": "https://files.pythonhosted.org/packages/a3/34/91ddb871d4bdc60240782a9e92ccc68b7b51f9d1df265291c58fa89b2e1e/bauhaus-1.1.4-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"md5": "63ccf373c35b7d2c0dba6d1a81499027",
"sha256": "d44f14fa1a33591456c80445ccce5ab87a9ac7dff64bfe8f8911e8b46b4c21f7"
},
"downloads": -1,
"filename": "bauhaus-1.1.4.tar.gz",
"has_sig": false,
"md5_digest": "63ccf373c35b7d2c0dba6d1a81499027",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.4",
"size": 16684,
"upload_time": "2022-12-13T05:05:22",
"upload_time_iso_8601": "2022-12-13T05:05:22.730141Z",
"url": "https://files.pythonhosted.org/packages/f9/71/862964f0ac099f8e4b92d1b930786c8a76d27a9115c6361ce6de558973b4/bauhaus-1.1.4.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2022-12-13 05:05:22",
"github": false,
"gitlab": false,
"bitbucket": false,
"lcname": "bauhaus"
}
JSON