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