Skip to content

Commit

Permalink
Merge pull request #76 from QuMuLab/dev
Browse files Browse the repository at this point in the history
official release info
  • Loading branch information
karishmadaga authored Dec 16, 2020
2 parents 3338424 + 4a1ddb5 commit 3ab4c18
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 73 deletions.
107 changes: 55 additions & 52 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
# Bauhaus

`bauhaus` is a Python package for spinning up propositional logic encodings from object-oriented Python code.

## Features
Expand All @@ -11,86 +10,90 @@
- 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
- With `python-nnf`, submit a theory to a SAT solver
- Theory introspection

## Installation

Install ``bauhaus`` by running
Install `bauhaus` by running
```
pip install bauhaus
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.
```
from bauhaus import Encoding, proposition, constraint
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.

e = Encoding()
```
Create propositional variables by decorating class definitions with ``@proposition``.
from bauhaus import Encoding, proposition, constraint
e = Encoding()
```
@proposition(e) # Each instance of A is stored as a proposition
class A(object): pass

Create propositional variables by decorating class definitions with `@proposition`.

```
Create constraints by decorating classes, methods, or invoking the constraint methods.
@proposition(e) # Each instance of A is stored as a proposition
class A(object): pass
```

# 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'))
Create constraints by decorating classes, methods, or invoking the constraint methods.

```
Compile your theory into conjunctive or negation normal form (note: the theory is truncated),
# 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'))
```

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)})})})
Compile your theory into conjunctive or negation normal form (note: the theory is truncated),

```
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)
```

e.introspect()
>>
constraint.at_most_k: function = A k = 2:
```
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.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.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)})
(~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)})})
...
...
Final at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})
...
...
```

## Contribute
Expand Down
43 changes: 22 additions & 21 deletions setup.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@

import io
from setuptools import setup
from setuptools import find_packages

Expand All @@ -18,38 +17,40 @@
}

CLASSIFIERS = [
"Intended Audience :: Science/Research",
"Topic :: Scientific/Engineering",
"Topic :: Scientific/Engineering :: Mathematics",
"Development Status :: 4 - Beta",
"Programming Language :: Python",
"Programming Language :: Python :: 3",
"Programming Language :: Python :: 3.4",
"Programming Language :: Python :: 3.5",
"Programming Language :: Python :: 3.6",
"Programming Language :: Python :: 3.7",
"Programming Language :: Python :: 3.8",
"Programming Language :: Python :: 3 :: Only",
'Intended Audience :: Science/Research',
'Topic :: Scientific/Engineering',
'Topic :: Scientific/Engineering :: Mathematics',
'Development Status :: 4 - Beta',
'Programming Language :: Python',
'Programming Language :: Python :: 3',
'Programming Language :: Python :: 3.4',
'Programming Language :: Python :: 3.5',
'Programming Language :: Python :: 3.6',
'Programming Language :: Python :: 3.7',
'Programming Language :: Python :: 3.8',
'Programming Language :: Python :: 3 :: Only',
]

with io.open('LICENSE', 'r', encoding='utf-8') as f:
with open('LICENSE', 'r', encoding='utf-8') as f:
LICENSE = f.read()

with open("README.md") as f:
with open('README.md', 'r', encoding='utf-8') as f:
LONG_DESCRIPTION = f.read()

LONG_DESCRIPTION_CONTENT_TYPE = "text/markdown"

setup(
name=NAME,
version=VERSION,
description=DESCRIPTION,
long_description=LONG_DESCRIPTION,
long_description_content_type=LONG_DESCRIPTION_CONTENT_TYPE,
classifiers=CLASSIFIERS,
author='Karishma Daga, Christian Muise',
author_email='[email protected], [email protected]',
license=LICENSE,
license="MIT",
description=DESCRIPTION,
long_description=LONG_DESCRIPTION,
long_description_content_type='text/markdown',
project_urls={
'Documentation': "https://bauhaus.readthedocs.io/",
'Source': "https://github.com/QuMuLab/bauhaus",
},
python_requires='>=3.4',
install_requires=DEPENDENCIES,
extras_require=EXTRAS,
Expand Down

0 comments on commit 3ab4c18

Please sign in to comment.