Enumerate all solutions to a subset of variables [CP-SAT]

[Ola Rozenfeld]

Hi!

I'm using CP-SAT to enumerate all feasible solutions, however in my problem there are variables that I "care about" and others are just "helper variables". A toy example: x,y,z with the constraint x=y, but I only want to enumerate all possible assignments to {x,y}.

So far, I found two ways to do that:

1. Run Solve(cp_model) in a loop, adding an Or constraint after every solution to fix at least one literal different to the current solution.

2. Run with the NewFeasibleSolutionObserver and iterate over all full assignments, computing a hash key for each one based on my key variables and thus merging the equivalent assignments manually.

Both of these seem quite inefficient, for different reasons. Is there another way I'm missing? I'd like to basically tell the solver to enumerate all assignments to a subset of variables.

Thank you!

Ola

[Mark]

I too have found myself doing this quite regularly over the years. 

Usually using approach 2 or something similar sufficed, but for problems with very large numbers of solutions it would be interesting to know whether there is a better 'recommended' approach, or whether an optional list of variables could be added as an argument to the solve() call specifying those that are cared about (seems like the most obvious API implementation).

[Eyal Gruss]

I guess this use case is common in or-tools due to e.g. control/selector booleans used in OnlyEnforceIf.

For my use case I found your second option to be much faster than the first one.

Eyal