# 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": null,
"name": "bauhaus",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.4",
"maintainer_email": null,
"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/f3/61/d3694733f1b47ba7dfa6cbb04dc40e501da2c2b18e91749213a3d03957fe/bauhaus-1.2.0.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.2.0",
"project_urls": {
"Documentation": "https://bauhaus.readthedocs.io/",
"Source": "https://github.com/QuMuLab/bauhaus"
},
"split_keywords": [
"logic",
"nnf",
"sat",
"constraints",
"encodings"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "f1b155d0de6cd37f2a4cec7211be4f967b74531afa6ede2076d6f725a6957ad8",
"md5": "26cce64e83c113bbf71c2157549640ba",
"sha256": "bcc11c7388a532d6f715ecc5ca0a7f8ee5f9b70f74b5f329bb1f50de61ea8767"
},
"downloads": -1,
"filename": "bauhaus-1.2.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "26cce64e83c113bbf71c2157549640ba",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.4",
"size": 16814,
"upload_time": "2024-09-11T01:00:49",
"upload_time_iso_8601": "2024-09-11T01:00:49.983862Z",
"url": "https://files.pythonhosted.org/packages/f1/b1/55d0de6cd37f2a4cec7211be4f967b74531afa6ede2076d6f725a6957ad8/bauhaus-1.2.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "f361d3694733f1b47ba7dfa6cbb04dc40e501da2c2b18e91749213a3d03957fe",
"md5": "a06e3231d86f09d065eb6514e7ea0d02",
"sha256": "f82f5f9a9c541831a883a8c14b8ee71121b53e3b7ad5db29c85032175b7240a1"
},
"downloads": -1,
"filename": "bauhaus-1.2.0.tar.gz",
"has_sig": false,
"md5_digest": "a06e3231d86f09d065eb6514e7ea0d02",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.4",
"size": 18386,
"upload_time": "2024-09-11T01:00:50",
"upload_time_iso_8601": "2024-09-11T01:00:50.950162Z",
"url": "https://files.pythonhosted.org/packages/f3/61/d3694733f1b47ba7dfa6cbb04dc40e501da2c2b18e91749213a3d03957fe/bauhaus-1.2.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-09-11 01:00:50",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "QuMuLab",
"github_project": "bauhaus",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "bauhaus"
}
JSON
