Soffit non-progress report #3

I finally figured out (I think) how to encode the "dangling condition" for graph rewriting into or-tools, but then it started crashing on me with some regularity.

I created a pull request: https://github.com/google/or-tools/pull/910 to or-tools which adds return values to some Python functions that were documented to have them.

The condition I want to create is a set of rules of the form:
"if X = 1, then (Y,Z) have to take the values (1,2) or (2,3) or (3,4)"
"If X = 5, then (A,B) have to take the values (0,5) or (7,12)"

The latter half of each rule can be represented by a TableConstraint which has a decent Python interface, AddAllowedAssignments. But how to hook it to a particular value of X?

One way would be to create a huge table of tuples that cover both X and all values for any other variables. But since in many cases values are "don't care", this would be enormous. (For example, X=1 only cares about Y and Z, and X=5 only cares about A and B.)

or-tools provides a way to make a constraint conditioned on a boolean variable. Unfortunately , X==1 is a LinearConstraint, not a boolean variable. But we can create a new boolean that's an "indicator" and use that to tie the two constraints together:

indicator1 = model.newBoolVariable( "indicatorX1" )
model.Add( X == 1 ).OnlyEnforceIf( indicator1 )
model.AddAllowAssignments( [Y,Z], [(1,2), (2,3), (3,4)] ).OnlyEnforceIf( indicator1 )
indicator5 = model.newBoolVariable( "indicatorX5" )
model.Add( X == 5 ).OnlyEnforceIf( indicator5 )
model.AddAllowAssignments( [A,B], [(0,5), (7,12)] ).OnlyEnforceIf( indicator5 )

Now we need to force some way of enforcing one and only one of the indicator values to be true. That's easy but non-intuitive:

model.Add( indicator1 + indicator5 == 1 )

If X=1 and X=5 are not the only possible values, we could add a third indicator variable requiring that X be equal to one of the other allowed values.

So, two or-tools bugs come into play here. The first (solved with the pull request above, and feasible to work around) was that AddAllowedAssignment did not return its Constraint object so that I could call OnlyEnforceIf on it.

The second is that the solver crashes on unsatisfiable instances. I tracked down why this is happening but don't know the code well enough to solve it: https://github.com/google/or-tools/issues/907

The crash bug pretty much makes it infeasible to release my project for other people to use. Even if I fix the C++ library, I would need a new release pushed to PyPi to make it easy to use the fixed version. So I'm contemplating whether I put the project on hiatus, or rip out or-tools and either write my own code to find graph matches, or use a different SAT library.

I did write a function to enumerate all surjective mappings, though. This function produces K-tuples that contain each of the input values at least once. These tuples can be thought of a function from the range [1,K] to the values, which is surjective ("onto").

def surjectiveMappings( k, values, optional=[] ):
    """Enumerate all the ways to select k distinct items from 'values' such that
    all values appear at least once."""
    if k < len( values ):
        return
    elif k == 1:
        if len( values ) == 1:
            yield (values[0],)
        else:
            for o in optional:
                yield (o,)

    # Pick a must-use, it becomes optional
    for i in range(len(values)):
        selected = values[i]
        for m in surjectiveMappings( k-1,
                                     values[:i] + values[i+1:], 
                                     optional + [selected] ):
            yield (selected,) + m

    # Pick a may-use
    for selected in optional:
        for m in surjectiveMappings( k-1,
                                     values, 
                                     optional ):
            yield (selected,) + m