CP-SAT certifies a wrong optimality proof on an all-linear model: adding one constraint lowers the certified optimum by 34% (9.15) #5293

What version of OR-Tools and what language are you using?

• OR-Tools: 9.15.6755 (Google.OrTools NuGet package)
• Language: C# / .NET 10
• OS: Windows 11 x64 (10.0.26200)

Which solver are you using?

CP-SAT

What did you do?

Solved an exported CpModelProto (90'770 variables, 86'541 constraints — every one of them linear) three ways with the same library and default parameters:

supply_dim_3_8 is an ordinary Boolean (domain [0,1], index 843). Runs B and C partition run A's feasible set, so A's optimum must be min(B, C) = 6'012'953 — yet A certifies 9'086'429 with a matching best bound (an optimality proof, not a gap-limit stop). The three certificates are mutually inconsistent by case analysis on a single Boolean, so at least one is wrong regardless of any external checking.

The contradiction also reproduces with num_search_workers:1, random_seed:1 (deterministic, single-threaded: run A returns the same OPTIMAL 9'086'429 in 21.5 s) and with num_search_workers:8.

Self-contained repro (proto + ~60-line runner + the three solver logs): https://github.com/jipjan/cpsat-915-wrong-optimal

git clone https://github.com/jipjan/cpsat-915-wrong-optimal && cd cpsat-915-wrong-optimal
unzip model.pb.zip
dotnet run -c Release -- model.pb solve default                     # -> OPTIMAL 9086429
dotnet run -c Release -- model.pb solve default supply_dim_3_8 1    # -> OPTIMAL 6012953
dotnet run -c Release -- model.pb solve default supply_dim_3_8 0    # -> OPTIMAL 9086429

The pin is added to the proto as a plain linear row before model construction — no assumptions, no hints.

Independent verification (no solver in the loop)

After each solve the runner verifies the returned solution against the original, unpinned file by plain Int128 arithmetic — every linear row evaluated directly (enforcement literals honoured, including negative literals; unenforced rows vacuously satisfied), every variable checked against its domain, the objective recomputed from Objective.Vars/Coeffs. Run B's solution passes: 45'475 enforced rows checked, 0 violations, all domains respected, objective recomputed = 6'012'953 exactly. So the point run B returns is feasible in the file run A was solved on and is cheaper than run A's certified optimum — run A's OPTIMAL is a false certificate.

Model characteristics

• All 86'541 constraints are linear; 41'106 rows carry enforcement literals.
• Objective: a single term, scaling_factor = 1, no domain, no offset, no floating_point_objective.
• No solution_hint, no search_strategy, no assumptions, no symmetry in the proto.
• The model is accepted by CP-SAT's model validation (no MODEL_INVALID).
• max |linear coefficient| ≈ 1.8e15; max |variable bound| = 1e10; per-row activity within int64.

The model is machine-generated (an air-handling-unit configuration MILP; the integer coefficients are scaled decimal cost data, which is where the large-coefficient / fine-granularity mix comes from). A CBC solve of the same underlying model and an independent brute-force enumerator both agree the true optimum is the 6'012'953 point.

What did you expect to see?

Adding a constraint can never improve the optimum: run A ≤ min(run B, run C). Expected OPTIMAL 6'012'953 for run A.

What did you see instead?

OPTIMAL 9'086'429 with best bound 9'086'429 — a certified optimality proof 51% above a solution the same solver finds (in 1.9 s) as soon as one Boolean is fixed to the value it takes in the true optimum.

Anything else we should know?

• Full log_search_progress:true logs for all three runs are in the repro repository (default parameters plus logging only). Solution fingerprints: A 0xef05b681612e39ba, B 0xf0ef5aa7e5a15806, C 0x43ce7204306f86a7.
• Possibly related past reports: CP-SAT solver returning non-optimal solutions with status "OPTIMAL" #3639 (non-optimal solutions returned with status OPTIMAL), CP-SAT assumes model unfeasible when minimizing objective with many similar coefficients / solving symmetrical problem #3620 and CP-SAT model that most of the time solved to optimality, but in rare cases it is determined to be infeasible #4839 (feasible models reported infeasible). We also observed the false-infeasible direction on a variant of this model (the same formulation with indicator slack rows closed).
• Happy to re-run against current main or any candidate fix.