qumulab / bauhaus Goto Github PK

I suggest adding some functionality that allows you to cleanly create custom constraints using the annotated objects. The functions provided with the library are incredibly useful, but trying to create custom constraints (even something as simple as negating a proposition) is clunky. Currently it seems like the only way to do it is to take care of the "abstract" annotated constraints first, then convert the theory to an NNF object and add extra constraints manually with an endless string of "&"s. Every proposition also has to be casted to an NNF variable, leading to a lot of verbose syntax for relatively simple statements.

Willingness to contribute

The Bauhaus Community encourages new feature contributions. Would you be willing to contribute an implementation of this feature?

• Yes. I can contribute this feature independently.
• Yes. I would be willing to contribute this feature with guidance from the Bauhaus community.
• No. I cannot contribute this feature at this time.

Proposal Summary

Both pypi and readthedocs deployments should be auto-magically triggered when a release is made.

Motivation

Because it's a pain to always remember how to re-deploy things.

Problem: A user may be changing the way they're instantiating annotated objects, but want the code and constraint decorators to remain the same.
Solution: Flush propositional variables in an encoding so that they can run the code again.

e = Encoding()
# do bauhaus things
theory = e.compile()
e.flush()

Example:

@constraint.exactly_one(e, groupby="a")
class A(object):
    def __init__(self, a, b):
        self.a = a
        self.b = b

Such that for each class object, we create a constraint exactly_one between all instances that share the same value for self.a.

TODO: Identify the following,
What should the user be able to do with this feature?

What would a user flow look like for this?

What would the expected output be?

Needs to be,

• easy to iterate over for get_inputs() function
• dups vs no dups?
• handles any given iterable as an argument

Need to access specific class instances stored in encoding.propositions (by class name) to apply the instance methods.
It's preferable to do this during constraint builder creation so that we're not offloading work in _ConstraintBuilder.get_inputs()

Look into using inspect.signature here.

A user can call this either as a decorator or as a function call.

If it's a decorator, they're likely assuming that left side = instance, right side = what is being returned.

So if they decorate a class,
@constraints.implies_all(e)
then we need a right hand side. For example,
@constraints.implies_all(e, right=Var(obj))
Then [all instances] -> right for the decorated class. If there's a left hand side, it would be added to the instance list such that,
[all instances] + [left] -> [right]

If they decorate a bound method, we assume that left: instance -> right: method return.

If they call the function like so,
constraints.implies_all(left = a, right = b)
then left -> right (simplest case).

I think we'll need to handle all of this in our construction of the _ConstraintBuilder in bauhaus/init.py so that we handle possible errors earlier.

Should be able to take an iterable of any valid types (annotated class, instance of that class, nnf.Var) and use in building constraint

• readthedocs website
• cleaned up technical architecture/specifications doc for the website
• contribution guidelines

Currently doing dict(key: obj, val: method(obj)). This is handy for implies_all, and if not, we can simply combine obj._var + keys._var

Could also do defaultdict(list) where each item is obj -> list

Equivalent to And(at_most_one, at_least_one)

Willingness to contribute

The Bauhaus Community encourages new feature contributions. Would you be willing to contribute an implementation of this feature?

• Yes. I can contribute this feature independently.
• Yes. I would be willing to contribute this feature with guidance from the Bauhaus community.
• No. I cannot contribute this feature at this time.

Proposal Summary

Ability to use compiled and simplified NNF statements in future constraints.

Motivation

I attempted to use bauhaus in an iterative algorithm, where the formulas needed to be compiled to NNF and simplified each time for use in the next iteration. However, I would run into the issue in the next iteration where I would need to combine a formula with bauhaus propositions with a compiled NNF formula, and as it stands you can only add constraints using bauhaus propositions. Below is a simple example of the error:

a = Bauhaus("a")
b = Bauhaus("b")
e.add_constraint(a | b)
# get NNF
f = e.compile()
# attempt to use it again, results in the error: 'And' object has no attribute 'compile'
e.add_constraint(f & (a | b))
e = e.compile()

Describe the solution you'd like
Ideally, the functionality to use either NNF statements or statements with bauhaus propositions (or both) as needed when adding constraints.

Why is it currently difficult to achieve this with Bauhaus?
Bauhaus currently only allows the user to add constraints using statements with bauhaus propositions.

At most K means at most K variables can be true.

Typically, the default for K is 1, but we should have no defaults here. Have the user provide K and we check if 1 <= K <= num of variables.

If K = 1, return at_most_one

See Successful SAT Encodings

Willingness to contribute

The Bauhaus Community encourages new feature contributions. Would you be willing to contribute an implementation of this feature?

• Yes. I can contribute this feature independently.
• Yes. I would be willing to contribute this feature with guidance from the Bauhaus community.
• No. I cannot contribute this feature at this time.

Proposal Summary

Proposition objects are created as unique, and so if you create multiple copies for various constraints, then it can lead to unintuitive bugs. By default, we should have a proposition be uniquely identified by it's representation (or a hash of that), and then we can create the object repeatedly and refer to the same proposition in the code.

Motivation

Is your feature request related to a problem? Please describe.

This shows what currently doesn't work, but should:

from bauhaus import Encoding, proposition, constraint

e = Encoding()

@proposition(e)
class V(object):
    pass

# Works: x refers to the same proposition
x = V('x')
y = V('y')
z = V('z')
E.add_constraint(x | y)
E.add_constraint(x | z)

# Doesn't work: each x is a unique proposition
E.add_constraint(V('x') | V('y'))
E.add_constraint(V('x') | V('y'))

While it doesn't seem like that much of a difference here, it can be largely problematic for large encodings with several variables.

Describe the solution you'd like

• Force implementers to define the method _prop_name on their objects using @proposition. If it's not there, throw an error.
• Return the outcome of this method for __repr__.
• Overload __hash__ and __eq__ appropriately (e.g., [this hack]).

Why is it currently difficult to achieve this with Bauhaus?
It's not implemented.

i.e. support for syntax
e.add_constraint(a >> b)

as it says!

Hey everyone,

Is there an easy way to create a big And/Or of a list of variables? I.e.

fluents = []
term = And(fluents) >> x_a

Thanks!

Originally posted by @eileenyyang in #94

• Testing for utlilities (bauhaus/utils.py)
• More testing for bauhaus/constraint_builder.py
• Add exceptions class

If A and B are classes with a @proposition annotation, then we may want to be able to write a constraint like...

e = Encoding()

@proposition
class A:
    pass

@proposition
class B:
    pass

b = B()
e.add_constraint(~A | b)

Interpretation would be that every instance of A is substituted in for a new version of this constraint at compile time.

Probably needs some advanced handling of the operator overloading (so that the class is considered an nnf.Var object, and a regular nnf constraint is built no matter what the arguments are).

Note that this is a far more advanced version of #87

Taking the results from a solved SAT theory with truth assignments, how can we present it to a user in a meaningful way.

Example: present truth values grouped by object types

It would be interesting to give a user different options for how they want to visualize it as well.

At least one variable is true is equivalent to a disjunction over all variables.
Or(variables)

Example use case:

class A:
@constraint.method(e)
def method():
pass

Currently not working with current implementation since the method needs to be called for the decorator to execute. Possible approach would be to detect in the decorator that the function is a bounded method, and if so, create a _ConstraintBuilder object from that.

At most one literal can be true.
And( Or( ~var_i, ~var_j ) ) for all i, j and i != j

where i and j are indices if you were to take the cross product of the variables.

groupby missing in readthedocs features, getting started, and on github readme

Could have the case where,

@proposition(e)
class A:
       @proposition(e)
       def method():
             pass

With the current implementation of @proposition, the decorator on an instance method only works when the method is invoked, not when a @proposition decorated class is instantiated. To support the above use case, we need the decorator to process instance methods at the stage when methods are defined but before the class is defined. At this stage methods look like functions. This is the exactly what the @constraint decorator supports.

• improved error handling by adding custom exceptions class for bauhaus (bauhaus/errors.py)
• removes current use of long strings in classes
• adds more informative naming of errors instead of the generic ValueError, etc
• we will be able to catch errors we expect and allow unexpected ones to bubble up during testing and from use
• errors always follow this pattern: (francois chollet, user experience design for APIs)
  1. Catch user errors early and anticipate common mistakes.
  Do user input validation as soon as possible. Actively keep track of common mistakes that people make, and either solve them by simplifying your API, adding targeted error messages for these mistakes, or having a "solutions to common issues" page in your docs.
  2. Provide detailed feedback messages upon user error.
  A good error message should answer: what happened, in what context? What did the software expect? How can the user fix it? They should be contextual, informative, and actionable. Every error message that transparently provides the user with the solution to their problem means one less support ticket, multiplied by how many times users run into the same issue.