I encountered behavior in the constraint solver I don't understand. I created a test case which I believed had only one solution, but I'm getting eight calls to OnSolutionCallback. (I'm using the Python wrappers.)
The model dumped by ModelProto() is generated by code I wrote, but looks as I expect it to. X1 through X4 represent selection of nodes from a graph. The first set of contraints are tags on the nodes (all nodes have the same tag.) The second set of constraints are edges, and I used unique tags to force a single working assignment. All the constraints are created with AddAllowedAssignments, and I call SearchForAllSolutions to start the search.
variables {
name: "X1"
domain: 0
domain: 4
}
variables {
name: "X3"
domain: 0
domain: 4
}
variables {
name: "X2"
domain: 0
domain: 4
}
variables {
name: "X4"
domain: 0
domain: 4
}
constraints {
table {
vars: 0
values: 0
values: 1
values: 2
values: 3
values: 4
}
}
constraints {
table {
vars: 1
values: 0
values: 1
values: 2
values: 3
values: 4
}
constraints {
table {
vars: 2
values: 0
values: 1
values: 2
values: 3
values: 4
}
}
constraints {
table {
vars: 3
values: 0
values: 1
values: 2
values: 3
values: 4
}
}
constraints {
table {
vars: 0
vars: 2
values: 0
values: 1
}
}
constraints {
table {
vars: 1
vars: 3
values: 4
values: 0
}
}
constraints {
table {
vars: 2
vars: 1
values: 1
values: 4
}
}
The callback gets this same solution eight times:
X1 0
X2 1
X3 4
X4 0
CpSolverResponse:
status: FEASIBLE
objective: NA
best_bound: NA
booleans: 51
conflicts: 0
branches: 14
propagations: 58
integer_propagations: 6
walltime: 0.001184
usertime: 0.001147
deterministic_time: 0.000008
Is this expected behavior? What can I do to better understand the behavior of the CP SAT solver?
Other, simpler, examples I tried have produced only the expected number of results. Removing the meaningless constraints from the model didn't change the behavior, nor did adding a second permissible edge.