Solved at Scale
Solved with CP-SAT
An external CP-SAT solver solves the pinned five-by-four instance under deterministic parameters and reports a provable optimum. The lesson quotes only the deterministic fields of the run: the status, the objective value, and the assignment itself.
Invocation
The invocation is cpsat_stream_solve solve basic_assignment.jsonl --params num_search_workers:1,random_seed:1, with the solution values written to a temporary --sol file. Why: a single search worker and a fixed seed make the run deterministic, so the solution quoted below is reproducible rather than anecdotal.
Solver result
The solver reports status OPTIMAL with objective value 265. Why: OPTIMAL means the solver proved a matching bound, not merely found a good solution. The output also carries timing, conflict, and branch counts; those fields are omitted here because they vary from run to run, and only the status, the objective value, and the assignment are deterministic.
The assignment
W1 takes T4, W2 takes T3, W3 takes T2, W4 takes T1, and W5 is idle. Why: each task is covered exactly once and the chosen cells sum to the certified objective. The labels are the diagram's own row and column headers.
Diagram note
Highlighted cells are the solver's assignment, and the idle worker row is marked by role, carrying the word idle. The cell entries are the original exact costs, not reduced ones. Pixel positions are rounded for layout; every number shown is exact.