bauhaus 1.2.0
Build logical theories for SAT solvers on the fly
License: MIT
Requires Python: >=3.4
Keywords: logic nnf sat constraints encodings

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