Register · Check 0031 · Scheduling
Does a roster satisfying all eight constraints exist for seven people?
No. Two weekends require eight distinct people. Proven infeasible, not searched and abandoned.
Outcome
Established
Published
09 September 2026
Question fixed
08 September 2026· stated by us, not proven
What came back.
No such roster exists. The model returns INFEASIBLE — a proof that the constraint set admits no satisfying assignment, not a search that ran out of time.
- Outcome
- INFEASIBLE
- Time to prove
- 0.089 s
- Same model, 8 staff
- OPTIMAL in 0.046 s — load 7 shifts each
- Same model, 7 staff, C8 removed
- OPTIMAL — feasible, and worse for the staff
The system under test.
The question is not whether a good roster exists. It is whether ANY assignment satisfies every hard constraint simultaneously. That is a question with a definite answer, and a solver can settle it either way.
- Horizon
- 14 days, starting Tue 1 Sep 2026
- Shifts
- Early · Late · Night
- Coverage required
- Early 2, Late 1, Night 1 — 4 per day, 56 over the fortnight
- Weekends in horizon
- 2 (days 5–6 and 12–13)
- Staff
- 7 named, 3 of them senior, each with stated unavailability
The stated constraints
- C1Every shift is covered by exactly the number of people required (Early 2, Late 1, Night 1)
- C2Nobody works more than one shift in a day
- C3At least 11h between shifts — no Early or Late the day after a Night
- C4Nobody works more than 5 consecutive days
- C5Stated unavailability is honoured
- C6At least one senior on every Night shift
- C7Nobody exceeds the fortnightly shift cap (9 shifts)
- C8Everybody gets at least one full weekend off
The second instrument.
Independence is a claim. The table below is the evidence for it — including the two things that ARE shared.
First instrument
CP-SAT constraint model
Boolean assignment variables over (person × day × shift), with the eight constraints expressed as linear constraints and a soft objective levelling the load. Asked to find any satisfying assignment.
Second instrument
An independently written checker
Takes only the FINISHED grid — a table of who works what — and re-derives all eight constraints from the constraint list. It never calls into the model, though it shares the file and the input constants — see the table below. For the infeasible case it verifies the pigeonhole argument arithmetically instead.
| Shared? | What | Note |
|---|---|---|
| Not shared | Constraint logic | The checker re-expresses each of the eight rules from the written constraint list. No function is called by both, and the checker never sees the model’s encoding. |
| Not shared | The solver | The checker performs no search. It is arithmetic over a finished table. |
| Shared | Source module | CORRECTED 10 Sep 2026. Both live in ONE FILE — identical sha256 — and an earlier version of this table claimed “no shared module, helper or constant”. That was false. There are no imports between them, but module scope is shared. |
| Shared | Constraint parameters | DEMAND (C1’s required counts), the consecutive-day cap (C4) and the horizon are module constants read by both. A wrong parameter is honoured identically by each. |
| Shared | Input data | Same staff, same availability. A wrong input produces a consistent wrong answer from both. |
| Shared | The constraint LIST | Both answer to the same eight written rules. A misread rule is reproduced by both. |
The reasoning
Five steps, each checkable without a computer.
This is the part that does not require you to trust the solver.
- 01Each weekend day needs four shifts covered.C1 requires Early 2, Late 1, Night 1 — four shift-slots on every day including Saturday and Sunday.
- 02Those four must be four DISTINCT people.C2 caps each person at one shift per day, so four slots on one day cannot be covered by fewer than four people.
- 03Nobody can staff both weekends.C8 gives everybody at least one full weekend off, and there are exactly two weekends in the horizon. So each person is available for at most one of them.
- 04Therefore two weekends require eight distinct people.The two weekend-staffing sets are disjoint, and each needs at least four members.
- 05The roster has seven.Eight distinct people are required and seven exist. No assignment can satisfy C1, C2 and C8 together. The remaining five constraints are not needed for the argument.
What this does not settle.
- It establishes infeasibility of THIS constraint set, not that the roster is unstaffable in practice.
- Relaxing any one rule may make it solvable. Removing C8 does, and the resulting roster is measurably worse for staff.
- Both instruments read the same eight written rules.
- If a rule is written down wrongly, both will faithfully honour the wrong rule. Independence is against implementation error, not against specification error.
- The staff data is fabricated for the example.
- The arithmetic is real and the solver run is real; the names and availability are not from a client.
- Only the infeasibility is proven, not the pigeonhole argument as the SOLE cause.
- The solver proves no assignment exists. The four-step argument above is a human explanation of why, verified by hand — a different rule set could be infeasible for a different reason.
What would change the conclusion.
- A weekend-coverage requirement below four shifts per day would break step 2.
- A horizon with three or more weekends would break step 3 — C8 would no longer force disjoint sets.
- Permitting a second shift in a day for one person would break step 2.
- An eighth person makes it feasible: verified, OPTIMAL in 0.046 s.
Artifacts
- identifiedConstraint model and independent checker
- One Python module containing the CP-SAT model and the separately written checker. Identified by content hash; not yet published as a downloadable file.
- sha256 d380b96c0eb634b3… · 12,045 bytes · examples/roster/solve_roster.py
- identifiedState generator
- Runs the model across every reachable control combination and writes the state file the site renders from.
- sha256 b4531ca187491f28… · 8,096 bytes · web/scripts/generate_roster_states.py
- identifiedGenerated state file
- The output of that run — every grid, status and timing quoted on this page and on the homepage demonstration.
- sha256 a0dc7eca493eebbf… · 10,102 bytes · web/lib/roster/states.json
- unavailablePublic download or versioned release
- No public repository, release tag or immutable record exists yet. Until one does, the hashes above identify the files we ran but do not let you fetch them.
- unavailableThird-party reproduction
- Nobody outside ProServiq has re-run this.
Revisions
09 Sept 2026
Published.
10 Sept 2026
Timing restated from 0.049 s to 0.089 s — the earlier figure was from a different machine and had been copied into prose rather than read from the run. The site now renders it from the generated state file.
10 Sept 2026
Independence table CORRECTED. It claimed the model and checker shared “no module, helper or constant”. Computing the artifact hashes showed both live in one file, sharing the input constants and the constraint parameters. Two rows moved from “not shared” to “shared”, and the limits section already stated the consequence.
A corrected figure stays in the record. Silently fixing one would make every other figure unverifiable.
Reproduce
Python 3.12, OR-Tools 9.15.6755
python scripts/generate_roster_states.py
Timing is machine-dependent; the outcome (INFEASIBLE at seven staff, OPTIMAL at eight) is not. The generator asserts both before writing.