Welcome to bauhaus!#

bauhaus is a library for building logical theories on the fly with Python.


  • 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

    • Arbitrary constraint specification over propositions

    • None of

  • Compile constraints into a theory in conjunctive or negation normal form

  • With python-nnf, submit a theory to a SAT solver

  • Theory introspection


Install bauhaus by running:

pip install bauhaus


Getting Started is the place to go to hit the ground running on using bauhaus.

The Module Reference documentation provides documentation for the library.


Head over to our Code of Conduct and get a feel for the library by reading our Architecture Design and Module Reference.


If you are having issues, please let us know. Reach out to us at karishma.daga@queensu.ca or by creating a GitHub issue.


The project is licensed under the MIT license for the Queen’s Mu Lab.