# CP-SAT returns a false INFEASIBLE at the root (0 conflicts, 0 branches) with `num_search_workers >= 10` and `cp_model_presolve = false`

**What happens.** On the attached model, CP-SAT reports `INFEASIBLE` while the model
has a solution. The verdict comes back at the root node, with `num_conflicts = 0`
and `num_branches = 0`, and `solution_info` empty. It only happens with presolve
turned off, and only from 10 search workers upwards. Below that threshold the same
file, same parameters, returns `FEASIBLE`/`UNKNOWN`.

Only two non-default parameters are needed:

```python
solver.parameters.cp_model_presolve = False
solver.parameters.num_search_workers = 24
```

## Reproduction

Everything is in the attached archive (`repro.py`, `model.pb.txt`,
`feasible_solution.json`, `verify_solution.py`). The model is a self-contained
export, no application code involved.

```console
$ python repro.py model.pb.txt
workers= 8 UNKNOWN wall= 20.260s conflicts= 262 branches= 18280 objective=-
workers= 9 UNKNOWN wall= 20.576s conflicts= 1422 branches= 10381 objective=-
workers= 10 INFEASIBLE wall= 2.455s conflicts= 0 branches= 0 objective=-
workers= 12 INFEASIBLE wall= 2.841s conflicts= 0 branches= 0 objective=-
workers= 16 INFEASIBLE wall= 2.690s conflicts= 0 branches= 0 objective=-
workers= 24 INFEASIBLE wall= 4.001s conflicts= 0 branches= 0 objective=-
```

The threshold at 10 workers is stable across runs and across the two machines we
tested. On the faster machine the false verdict comes back in 0.04–0.07 s; the
seconds above are mostly model loading.

## The model is feasible

`feasible_solution.json` holds a full assignment for the 5776 variables, found by
the same solver on the same file with 16 workers and presolve on. Pinning every
variable to its value reduces the model to a consistency check, and that check
passes with a single worker, no search involved:

```console
$ python verify_solution.py model.pb.txt feasible_solution.json
5776 variables pinned, 1 worker(s): OPTIMAL in 0.215s, objective=33423490306.0 (expected 33423490306.0)
```

So the model has a solution, and the `INFEASIBLE` above is wrong.

## Where it comes from

With `log_search_progress = true`, the failing run marks four subsolvers as done
during the loading phase, at the exact time of the verdict:

```text
Starting search at 0.01s with 24 workers.
15 full problem subsolvers: [core, default_lp, fixed, lb_tree_search, max_lp, no_lp,
objective_lb_search, objective_shaving_max_lp, objective_shaving_no_lp, probing,
probing_max_lp, pseudo_costs, quick_restart, quick_restart_no_lp, reduced_costs]
9 first solution subsolvers: [fj(3), fj_lin, fs_random, fs_random_no_lp(2),
fs_random_quick_restart, fs_random_quick_restart_no_lp]

#Done 0.02s probing_max_lp [loading]
#Done 0.02s reduced_costs [loading]
#Done 0.02s lb_tree_search [loading]
#Done 0.02s probing [loading]
...
status: INFEASIBLE
```

Those `[loading]` completions are the signal, and the correlation is exact. Over 39
runs on this instance (varying worker count, portfolio and sharing parameters), all
21 `INFEASIBLE` verdicts had at least one subsolver finishing at `[loading]`, and all
18 runs that ended `FEASIBLE` or `UNKNOWN` had none. The six subsolvers ever seen
finishing there are `probing`, `probing_max_lp`, `probing_no_lp`, `reduced_costs`,
`lb_tree_search` and `objective_lb_search_max_lp`.

At 10 workers the portfolio is
`[core, default_lp, fixed, max_lp, no_lp, quick_restart, reduced_costs]` — one name
more than at 9 workers, and that name is `reduced_costs`.

Ablation over the same instance, 24 workers, presolve off, 20 s budget, forcing the
portfolio through the `subsolvers` parameter. Let `BASE6` be
`[core, default_lp, fixed, max_lp, no_lp, quick_restart]`, i.e. the full-problem
subsolvers CP-SAT itself picks at 9 workers:

| portfolio | verdict |
| --- | --- |
| default (15 full-problem subsolvers) | **INFEASIBLE, 0.043 s** |
| `BASE6` + `probing` | **INFEASIBLE, 0.046 s** |
| `BASE6` + `probing_max_lp` | **INFEASIBLE, 0.064 s** |
| `BASE6` + `reduced_costs` | **INFEASIBLE, 0.045 s** |
| `BASE6` + `lb_tree_search` | **INFEASIBLE, 0.045 s** |
| `BASE6` + `objective_lb_search` | UNKNOWN |
| `BASE6` + `objective_shaving_max_lp` | UNKNOWN |
| `BASE6` + `objective_shaving_no_lp` | UNKNOWN |
| `BASE6` + `pseudo_costs` | UNKNOWN |
| `BASE6` + `quick_restart_no_lp` | UNKNOWN |
| `BASE6` alone | FEASIBLE, objective 24 707 072 598 |
| `BASE6` + `probing`, presolve **on** | FEASIBLE |

Any single one of `probing`, `probing_max_lp`, `reduced_costs`, `lb_tree_search` added
to a healthy portfolio is enough to produce the false verdict. The rows that are not
`INFEASIBLE` do vary between `FEASIBLE` and `UNKNOWN` from run to run, as expected
from an asynchronous portfolio and a 20 s budget; what does not vary is which
portfolios produce the false verdict, and it comes back in under 0.1 s every time.

`ignore_subsolvers` does not help, and the log says why: the freed slots are filled
with sibling variants that behave the same way. Excluding
`probing, probing_max_lp, probing_no_lp, reduced_costs, lb_tree_search` still gives
`INFEASIBLE` in 0.052 s, and this time the subsolver finishing at `[loading]` is
`objective_lb_search_max_lp`, which the portfolio pulled in to replace them. Note
that plain `objective_lb_search` is one of the safe entries in the table above; its
`_max_lp` variant is not.

An explicit whitelist works. The 11-subsolver portfolio
`[core, default_lp, fixed, max_lp, no_lp, objective_lb_search, objective_shaving_max_lp,
objective_shaving_no_lp, pseudo_costs, quick_restart, quick_restart_no_lp]` never
produced `INFEASIBLE` in 7 runs at 16 and 24 workers (2 × FEASIBLE, 5 × UNKNOWN);
with that list the log shows no `[loading]` completions at all.

## Ruled out

All of these still return the false `INFEASIBLE` at 24 workers with presolve off:

* `linearization_level = 0`
* `symmetry_level = 0`
* `share_level_zero_bounds = false`
* `share_binary_clauses = false` + `share_glue_clauses = false`
* `share_objective_bounds = false`
* `use_probing_search = true` on a `BASE6` portfolio, on the other hand, does **not**
reproduce it — so it is not the probing algorithm as such, but the subsolver
instances that run it during loading.