google / google/or-tools

CP-SAT: uncaught std::out_of_range (absl::btree_map::at) in SolutionCrush::SetOrUpdateVarToDomainWithOptionalEscapeValue aborts the process during presolve

Open
#5,288 7 comments 1 reaction 2 assignees Claimed by @Mizux View on GitHub
Bug Solver: CP-SAT Solver
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.