Optimization with Python: Infeasibility Explanation for Integer Programming with Google OR Tools
TL;DR
There is no direct interface implemented for infeasible detection for Mixed Integer Programming, but here’s a workaround provided by OR-Tools developers using the CP-SAT solver with the OR-Tools ( >= 8.2 version).
In this workaround, we convert the Integer Problem into a Constraint Programming problem, by adding a boolean variable (called enforcement literal) corresponding to each constraint, which suggests if the constraint is enforced or not. The CP-SAT solver will heuristically find a (local) minimum assignment of false enforcement literals to get a feasible model. We will then check which enforcement literal is False and thus find which constraint is infeasible/conflicting with others.
One remaining problem is that the solver will output all conflicting constraints, which could be a large list, even though there might be only one constraint that is incorrect. We might need to go through all the infeasible constraints to find out which one to modify, or maybe check feasibility every time we add a set of constraints to avoid going through a large list of constraints.
Brief Background about Constraint Programming and CP-SAT
Google provides a few ways to solve CP problems:
- CP-SAT solver: A constraint programming solver that uses SAT (satisfiability) methods.
- Original CP solver: A constraint programming solver.
Constraint Programming is based on feasibility (finding a feasible solution) rather than optimization (finding an optimal solution) and focuses on the constraints and variables rather than the objective function. In fact, a CP problem may not even have an objective function — the goal may simply be to narrow down a large set of possible solutions to a more manageable subset by adding constraints to the problem.
The CP-SAT solver returns one of the status values shown in below table:
These are defined in cp_model.proto.
Intuition
In the general sense, it might not be the right approach to throw a series of constraints on a solver and ask the solver to find what is infeasible. The better approach is to instrument your code with a series of boolean values corresponding to the constraints we have. That is, each inequality has enforcement literal.
Then we want a minimal number of false literal to get a feasible model, or maximize the sum of enforcement literals to get a feasible model. We can either set minimizing the (weighted) sum of literals as the objective function, or we can add these enforcement literals as assumptions, a functionality supported by OR-Tools CP solver, into the model. Then we can use the CP solver in OR-Tools which will try to heuristically find a (local) minimum assignment of false literals to get a feasible model.
Approach
Steps of Implementation
1. add boolean variables corresponding to each constraint, which is defined as enforcement literal in OR-Tools. In the end, we want to achieve:
enforcement_literal_1 => constraint_1
enforcement_literal_2 => constraint_2
…
enforcement_literal_n => constraint_n
2. add enforcement literal to a constraint, we can use the function OnlyEnforceIf(), defined as followed:
This method adds one or more literals (that is, a boolean variable or its negation) as enforcement literals. The conjunction of all these literals determines whether the constraint is active or not. It acts as an implication, so if the conjunction is true, it implies that the constraint must be enforced. If it is false, then the constraint is ignored. BoolOr, BoolAnd, and linear constraints all support enforcement literals.
Notice that in OR-Tools only supports enforcement literals for linear constraints, boolean constraints, and intervals.
3. add enforcement literal to model as assumptions using model.Assumptions()
4. call CpSolver() to solve the model
5. call solver.SufficientAssumptionsForInfeasibility() to display infeasible literal, which would be the infeasible constraints
Implementation Example
Create an infeasible model that constrains every variable to be larger than the others:
