CP-SAT: Workarounds for OnlyEnforceIf with Linear Expressions

Question

Background

I've written a solver that selects a subset of people from a larger pool such that the subset has at least X people per attribute (Gender/Job/Country etc. X differs per attribute).

This involves two dataframes: 1st is a DF of people with columns corresponding to various attributes (Gender, Job, etc), 2nd is a DF of requirements. This DF has 3 columns: The column to reference in the first DF, the specific attribute and minimum people required ie ["Job", "Doctor", 10]. Then the desired subset size is given and the solver tries to find a subset that fulfils each requirement.

My implementation currently has a boolVar AttributeSelectionMap[(i,j,k)] which is 1 if Person i, Column j, Attribute k is selected (Linearizations for Person i being selected and Person i has Attribute k on Column j are written as well but not included here).

Then for each minimum target to meet, I have

for j in columns:
    for k in columnAttributes:
        model.Add(sum(AttributeSelectionMap[(i,j,k)] for i in People) >= minimumtarget

The solver works fine with all the linearizations etc solving for which person in the list of People to pick for the subset.

Question I'm now trying to implement a way to figure out which constraints are causing Infeasible scenarios. The general idea is similar to the one laid out here: https://github.com/google/or-tools/issues/973

Basically, I'd like to add a boolVar per minimum target constraint that is 1 when the constraint has been met, and 0 otherwise. Then I would have the solver maximize these boolVars such that even if it were Infeasible I could figure out from the 0s which constraints caused the Infeasible outcome.

The intended implementation was as such:

constraintgrid = {}
constraintcount = 1

for j in columns:
    for k in columnAttributes:
        model.Add(sum(AttributeSelectionMap[(i,j,k)] for i in People) >= minimumtarget)
        constraintgrid[constraintcount] = model.NewBoolVar(f"Constraint {constraintcount}: {k} needs minimum {minimumtarget}")
        model.Add(constraintgrid[constraintcount]).OnlyEnforceIf(sum(AttributeSelectionMap[(i,j,k)] for i in People) >= minimumtarget)
        constraintcount += 1

The implementation above runs into the bug "NotImplementedError: Evaluating a LinearExpr instance as a Boolean is not implemented.", so the sum(target) >= minimumtarget part is causing the bug.

Are there any existing workarounds for this where I could make this "constraint variable" work that doesn't involve using OnlyEnforceIf on a linear expression?

Answer 1

This is a recurring question, and I have written a page of doc to solve it:

https://github.com/google/or-tools/blob/stable/ortools/sat/docs/channeling.md

The idea is to create a Boolean variable that is equivalent to your linear condition, and use it in the OnlyEnforceIf as it accepts only one or more Boolean literals.

in a nutshell:

  cond = model.NewBoolVar('cond')

  # Link the condition with the linear expression.
  model.Add(my_sum >= minimum_target).OnlyEnforceIf(cond)
  model.Add(my_sum < minimum_target).OnlyEnforceIf(cond.Not())

  # Use the condition variable. Use implications as this is shorter
  model.AddImplication(cond, constraintgrid[constraintcount])
```