CP-SAT: uncaught std::out_of_range (absl::btree_map::at) in SolutionCrush::SetOrUpdateVarToDomainWithOptionalEscapeValue aborts the process during presolve
- Dominant language
- C++
- Stars
- 14.1k
- Forks
- 2.5k
- Avg merge
- 8h 39m
- Merged PRs (30d)
- 72
Description
*Transparency note: this issue was investigated, patched, and written
by Claude (Fable 5), an AI assistant working on our production planning
system, under human direction; the human operator reviewed and filed
it. The crash, the patch, and the benchmark results are from real runs
on our workload.*
**Version**: or-tools 9.15 (Homebrew bottle and source build), macOS
14 arm64, CP-SAT via the C++ API (multi-worker solve with a solution
hint, `repair_hint` default).
**What happens**: during presolve of a large industrial CP-SAT model
(~600k variables, day-granular scheduling encoding, complete solution
hint), a solver worker terminates the whole process:
```
libc++abi: terminating due to uncaught exception of type
std::out_of_range: absl::btree_map::at
```
The failure is nondeterministic across runs of the same model (it
depends on which presolve path a worker takes), which makes it
particularly painful in long solves.
**Where**: `ortools/sat/solution_crush.cc`,
`SolutionCrush::SetOrUpdateVarToDomainWithOptionalEscapeValue`:
```cpp
SetLiteralValue(encoding.at(new_value), true);
```
The function's own doc comment (solution_crush.h) enumerates
"3/ The hinted value is not in the domain, and there is no escape
value." — in exactly that case `new_value` is derived via
`ValueAtOrBefore/After` from the reduced domain, and nothing guarantees
the `encoding` map carries a literal for it. When it does not, `.at()`
throws, and since this runs inside a worker thread the exception is
never caught: the entire process aborts.
**Why the fix is safe**: SolutionCrush maintains the solution *hint*
through presolve transformations; it never affects correctness of the
search. Skipping an uncrushable entry merely leaves one hint value for
solver-side hint repair — strictly better than terminating the process.
**Patch** (running in production since 2026-08; the exact
configuration that aborted stock at ~6 minutes completed a full 20-min
stint under the guard, with objective parity on our benchmarks):
```diff
--- a/ortools/sat/solution_crush.cc
+++ b/ortools/sat/solution_crush.cc
@@ -256,7 +256,14 @@ void SolutionCrush::SetOrUpdateVarToDomainWithOptionalEscapeValue(
new_value = reduced_var_domain.ValueAtOrAfter(old_value);
}
- SetLiteralValue(encoding.at(new_value), true);
+ const auto encoded = encoding.find(new_value);
+ if (encoded == encoding.end()) {
+ // The reduced domain admits `new_value` but the encoding carries
+ // no literal for it: crushing this hint entry is impossible.
+ // Leave the hinted value for solver-side hint repair instead of
+ // throwing std::out_of_range out of a worker thread.
+ return;
+ }
+ SetLiteralValue(encoded->second, true);
CHECK(!encoding.contains(old_value));
SetVarValue(var, new_value);
}
```
I cannot share the triggering model (proprietary industrial data), but
the defect is visible from the code path alone: case 3 of the
function's contract reaches an unguarded `.at()`. Happy to test a
candidate fix against our workload.
Contributor guide
Assessment
This issue has not been assessed yet.