Solver Strategy

A proposal, not a decision. Every entity and relationship below is open to challenge; the open decisions are listed at the end.

Version 0.1, 6 September 2026. Answers: "timetabling is NP-complete; what makes it tractable so we can actually do anything?" Numbers are measured on Mevo Hagalil with the engine in apps/engine (OR-Tools CP-SAT 9.15, 8 workers, laptop).

Overview

NP-completeness is a statement about the worst case of the general problem; nothing we do removes it. What we can do is hand the solver instances that are not the worst case, never ask for a proof of optimality, and keep a human in the loop for the decisions that are really human. The research brief (section 4) names four reasons real timetables get built: propagation, clause learning, slack, and anytime search. This document turns those into engineering choices for Mevo Hagalil and reports what they buy.

Summary

• Fix what is already decided. Homeroom pairing, the 22 pre-placed programme events, staff meetings and part-time days are data, not variables. That removes about a third of the freedom before search starts.
• Decompose. Who teaches which class is a human decision made before solving. The solver only places events in time. Rooms come after, as a separate small problem, if the school needs them at all.
• Let CP-SAT do what it is good at: propagation, clause learning and a portfolio of LNS workers, with a time limit and a hard-first, soft-second objective.
• Never restart from nothing. Warm-start from last week's timetable; repair with a stability term so a mid-year change moves a handful of lessons, not the school.
• Measured: 570 events, 14,096 start variables, 17,675 booleans, 7,460 constraints. First feasible timetable in 0.3 s. Soft cost 104 after 5 s, 64 after 30 s, 28 after 60 s, against 214 for the hand-made timetable, which also contains one double booking.

Bottom line

Mevo Hagalil is a small, slack instance once the fixed structure is removed, and CP-SAT solves it to a better score than the hand-made timetable in under a minute. The product should show a first feasible timetable within seconds and improve it in the background; it should treat "prove optimal" as a non-goal. The risk is not solver speed but data quality: subjects, hour baskets and the identity of the co-teaching specialists are missing, and without them three of Vegman's rules cannot be enforced at all.

Detailed explanation

(a) Fixing what is already decided

The importer produces 570 events for 594 class-slots. 33 are fixed in time by the school's own programmes (S-05 to S-07: choir, orchestras, mentoring, the grade-5 Tuesday block, meetings, no-class gym and music slots) and are pruned to one start each. Homeroom pairing (S-02) is inferred once and stored on Class and Staff; it never becomes a variable. Grade-team meetings become unavailable rows on the three homeroom teachers of that grade; part-time days (R-09) become whole-day unavailable rows inferred from the export. These land as domain pruning: a hard availability row deletes start variables instead of adding constraints, so a part-timer on two days has 14 starts per lesson, not 33.

(b) Decomposition into stages

1. Staff to class is a human decision (which teacher takes ג' נשר mathematics) and stays one. The importer reads it from the export; the back-office will let Vegman edit it. This is where the combinatorics would explode (45 staff × 570 events) and exactly the stage a deputy head wants to own.
2. Time assignment is the solver's job: 570 events into 33 slots, subject to clashes, availability and the R rules. This is what the numbers above measure.
3. Room assignment, when Q-13 says it is needed, is a bipartite matching per slot, solvable independently and near-instantly once times are known. Kristiansen et al. (2015, brief reading 9) show the two-step split costs little on XHSTT instances.

Each stage is small because the others are fixed while it runs. A StaffSlot with staffId: null is stage 1 work left undone, not a request for the solver.

(c) Propagation and clause learning

Every class has exactly 33 lessons for 33 slots, so the per-class AtMostOne constraints are tight packings: placing one lesson removes that slot for 32 others. Staff clashes propagate across classes. At a dead end CP-SAT learns a clause naming the combination that failed and never revisits it (brief section 4). The observable effect is 0.3 s to first feasible: propagation collapses most of the 14,096 start variables before branching.

(d) Anytime search

The solver runs with a time limit and 8 workers and reports each improving solution through a callback (elapsed, objective, bound, phase). Hard constraints are true constraints, so the first solution already has hard = 0; the objective is the weighted soft cost. The UI should show the phase (searching, then improving), the current soft cost by constraint type, the lower bound (10 here: no timetable can score below 10), and a "use this now" button at every point. Measured trajectory from scratch: 104 at 5 s, 93 at 10 s, 64 at 30 s, 28 at 60 s.

(e) Warm start and minimal-perturbation repair

AddHint seeds the search with the previous timetable. On this instance it makes no measurable difference to time-to-feasible (0.31 s versus 0.30 s) because feasibility is already trivial, and it does not keep the solution close: the hinted run still moved 492 of 570 events, because nothing in the objective rewarded staying put. Repair therefore adds a stability term: a penalty per event that leaves its previous slot, plus pinning for events the user has locked. This is the classical minimal-perturbation formulation (brief section 5, MaxSAT CPAIOR 2020) and the mechanism for mid-year changes: a teacher leaves, her lessons are reassigned in stage 1, and the solver moves the fewest lessons that restore hard = 0. Fix-and-optimize (Dorneles et al. 2014) is the same idea applied by the solver to itself: CP-SAT's LNS workers relax a neighbourhood, re-solve, and keep the improvement. Measured repair from the hand-made timetable (weight 1 per move, 30 s): 35 of 570 events moved, hard 1 to 0, soft 214 to 141, with a proven bound of 134 on the combined objective.

(f) Symmetry and dominance

Slots on the four seven-period days are interchangeable for most events, and so are the five weekly lessons of one course. Both create symmetric solutions that waste search. Data breaks the first kind partly (fixed events, meetings and the short Tuesday make days distinct); CP-SAT's symmetry detection handles the rest. The second kind is handled by generating same-course events as an EventGroup spread over days, which makes them distinguishable; when the curriculum arrives (N-03), lexicographic ordering within a course removes the remaining permutations.

(g) Effective size and solve times

Measured on 6 September 2026 after Vegman's answers were applied (requirements v0.3, engine README "Applied answers").

The hand-made score by type: no-clash 0 (the ליבנה double booking was a stale cell, S-17); no-gaps hard 3, the excess over the weekly gap budget of Q-04 for two small posts (רותם 3 gaps against a budget of 2, יפעת 2 against 0) whose individual and staying hours are estimated from the export and are probably wrong at that scale; ends-long-day 115 (18 teachers not at their R-07 target, 9 of them part-timers whose proportional target is pending Q-24); room-shared-owners 54 (the gym owners אתי and רגב teach simultaneously in 11 periods, the music-shelter owners נגה and שני in 7); homeroom-starts-first-period 5 (סתו opens her own class twice); availability, fixed-time, block-at-periods, spread-over-days, room-owner-whole-class all 0. Total gaps are 106 against a total budget of 306, so the gap rule, now hard, leaves the solver a lot of room: the optimum of 53 has no gap violation at all. What remains at the optimum is structural: אתי teaches every period of her two days while רגב teaches 26 of 33, so some gym overlap is unavoidable, and the part-time long-day targets.

(h) What makes an instance hard, and the fallback

Hardness comes from tightness, not size: part-timers whose few days coincide with everyone's fixed blocks, many grade-wide linked blocks on distinct days, scarce specialist rooms (brief section 4). When the hard constraints cannot all hold, INFEASIBLE alone is useless to a deputy head. The engine rebuilds the model with one assumption literal per constraint family (each staff member's availability, each class's clash set, each fixed event, each block rule) and asks CP-SAT for a sufficient set of assumptions for infeasibility. The result is a short list such as "availability אתי; fixed-time ev-orchestra-thu-6; no-clash class ג' בז" naming the smallest conflicting set found: the pattern the brief recommends (section 5, TRACE-cs), where the solver computes the explanation and language only translates it.

(i) The constraint catalogue as data

Every rule is a row: type, hard, weight, params, appliesTo, implements. Each type has a scorer that evaluates any Timetable without a solver; the CP-SAT adapter mirrors the same definitions. Because the scorer is independent, the solver can be audited: on every run so far the model objective equals the catalogue's soft score exactly. Eight types are implemented; subject-per-day, double-period and avoid-last-period are registered and return a note until subjects (N-01), the curriculum (N-03) and the x/y/z list (Q-09) exist. A new rule is one scorer and one model fragment; the domain is untouched.