vac-optimizer/docs/research/leave-planning-solver.md

Solver for leave placement

Research date: 2026-08-28.

Recommendation

Do not add a solver dependency. highs (HiGHS compiled to WebAssembly) was the only candidate reviewed that combined browser execution, TypeScript declarations, MILP, a permissive licence, recent maintenance, and a package size compatible with lazy loading. The throwaway spike nevertheless failed the performance gate for the agreed 12-month model.

Keep a deterministic dependency-free planner and return PlanningIncomplete when it cannot finish all quality stages within the budget. Do not introduce a backend merely to gain OR-Tools, and do not move to the much heavier Z3 fallback.

This assessment also accounts for support risk: the upstream HiGHS documentation lists highs-js as a browser interface but says that some listed interfaces are community-contributed and not officially supported by the HiGHS team (HiGHS interfaces). The wrapper's own repository is therefore the primary source for its JavaScript contract.

Spike result

The standalone 4,687,975-byte prototype is preserved on branch prototype/highs-leave-planner at commit f184a29. It embeds the 3,431,156-byte Wasm module, runs HiGHS in a Worker, exposes the five guided scenarios plus editable JSON, and terminates the Worker at the hard 10-second limit.

Measurements below used Node 24 and the same embedded Wasm/model code on the development machine. They are not phone benchmarks; because the representative cases already miss the hard limit there, the inference is that they cannot satisfy the stricter mid-range-phone gate.

Scenario	Outcome	Elapsed	Last stage
Representative year	PlanningIncomplete	10,098 ms	Longest work sequence, time limit
Typed obligations	Plan	479 ms	All stages optimal
Chained earned entitlements	Plan	418 ms	All stages optimal
Contradictory obligations	PlanningConflict	56 ms	Core model infeasible
Loaded year	PlanningIncomplete	10,087 ms	Longest work sequence, time limit

The embedded Worker was also executed directly as a self-check: the typed case returned Plan and the contradictory case returned PlanningConflict. Cold Wasm initialization measured 19 ms on this machine, separately from solve time. Angular integration, memory profiling, and a phone run were intentionally skipped once the more fundamental solve-time gate had failed.

Why HiGHS was the best candidate

The published highs package compiles HiGHS to WebAssembly, works in Node.js and modern browsers, includes TypeScript declarations, supports LP/MILP, loads its .wasm asset explicitly, and has a Worker demo (highs-js repository, npm package). HiGHS and the wrapper are MIT-licensed (HiGHS source, highs registry metadata). Version 1.15.2 has an npm dist.unpackedSize of 3,525,070 bytes; this is installed size, not transfer size or Angular initial-bundle cost, so the spike must still measure the production build.

HiGHS supports binary and integer variables and reports optimal/infeasible/time-limit statuses (variable and model statuses). Its core supports prioritized lexicographic linear objectives when blend_multi_objectives is false (multi-objective optimization). If the stable JS surface used by the spike does not expose that core API, use repeated solves: optimize criterion 1, add an equality fixing its integer optimum, then optimize criterion 2. Do not replace the order with hand-tuned weights.

The agreed domain maps to a bounded MILP for at most one year:

• binary placement[balance, workingDay] variables enforce at most one leave placement per working day, type compatibility, availability, expiry, and balance capacity;
• obligation occurrences become hard linear constraints; ordered preference satisfactions become successive integer objectives;
• an IF_THEN completion Boolean activates a virtual earned entitlement whose capacity is rewardDays * completion, with dates restricted to the day after acquisition through one year later;
• because an earned entitlement is only available after its generating period, these activations are time-directed and cannot finance themselves;
• time-off starts, total calendar duration, the longest work sequence, and deficits of internal work sequences shorter than five working days can be represented with additional binary/integer variables and standard linear implications;
• shared placements need no ownership: each compatible rule-satisfaction Boolean can refer to the same placement variables.

The highest-risk part was not typed balances or obligations; it was the linearization of period boundaries and work-sequence objectives. The spike tested that formulation without building a generic solver abstraction.

For PlanningConflict, HiGHS exposes irreducible-infeasible-subsystem data in its native API (HighsIis), and the current wrapper repository documents getIis in its persistent API (highs-js API map). If that API is not in the chosen stable package, a deletion filter over the small set of obligation rules is sufficient: repeatedly solve after removing one obligation and return a sufficient conflicting subset. This is application logic, not a reason to add another solver.

Candidate comparison

Candidate	Browser / TypeScript	Lexicographic optimization	Licence and maintenance	Decision
HiGHS via highs	WebAssembly for modern browsers, Node, TypeScript declarations; .wasm must be served as an asset (wrapper README)	Native prioritized linear objectives in HiGHS; sequential exact integer objectives are a fallback (HiGHS guide)	MIT; highs 1.15.2; 3,525,070 bytes unpacked (registry metadata)	Reject after spike: misses hard limit
Z3 via z3-solver	Official high- and low-level TypeScript bindings and browser build; Z3 ships as Wasm (official published README)	Optimize defaults to objective declaration order (Z3 guide)	MIT; z3-solver 5.2.0; 35,820,846 bytes unpacked (registry metadata)	Do not choose now
MiniZinc official JS	Official TypeScript/browser API runs WASM in a Web Worker and requires separate worker, WASM, and data assets (official repository)	Expressive constraint language, but VacOptimizer would still need an explicit staged objective and a second source language	MPL-2.0; minizinc 4.5.1; 18,651,774 bytes unpacked (repository, registry metadata)	Do not prototype: no demonstrated benefit over the smaller HiGHS path
OR-Tools CP-SAT	Officially supported only in C++, Python, Java, and .NET; there is no official JS/browser distribution (installation guide)	Strong semantic fit for Boolean/integer scheduling; integer-only constraints and objectives (CP-SAT guide)	Apache-2.0 and actively released (repository, releases)	Reject for this client-only app
GLPK via glpk.js	Browser/Node WebAssembly port with a JSON LP/MILP API and TypeScript types (project repository)	Published API exposes one linear objective; exact priority therefore needs repeated solves (API)	GPL-3.0; 2,616,261 bytes unpacked for 5.0.0 (registry metadata)	Reject; no material advantage over MIT HiGHS
Choco Solver	Java library distributed through Maven; no official TS/browser binding (project repository)	Constraint programming is a semantic fit	BSD-3-Clause and recently maintained (project repository)	Reject for this architecture
Timefold Solver	Official open-source solver targets Java and Kotlin, with JVM/Maven setup (project repository, quickstarts)	Multi-level planning scores fit ordered quality goals, but its search is a much larger application model than this bounded MILP	Apache-2.0 and recently maintained (project repository)	Reject for this architecture
No dependency	Native TypeScript, no loading or licensing cost	A deterministic planner can follow ordered criteria but may need to report incomplete optimization instead of claiming global optimality	Owned entirely by VacOptimizer	Adopt

Why not Z3

Z3 is the strongest alternative semantically: Boolean implications make earned rights and rule completion natural, arithmetic over integers avoids MILP tolerances, and its optimizer is lexicographic by default. Its official browser package, however, requires threads and SharedArrayBuffer; browsers must receive special headers, and the Emscripten worker script must be served separately rather than bundled normally (official TypeScript binding limitations). At 35.8 MB unpacked it is also roughly ten times the installed size of highs (registry metadata). Those deployment constraints buy expressiveness the leave model does not currently need.

Spike acceptance check

Use one throwaway implementation, no framework layer:

1. Encode 365 calendar days / roughly 260 working days, several dated CP/RTT/Other balances, overlapping typed obligations and preferences, and at least two chained earned-entitlement occurrences.
2. Compare criteria lexicographically: jointly valid obligations, minimum at-risk loss, each preference in user order, maximum non-working-day gain, minimum longest work sequence, minimum short-sequence deficit, minimum supporting placements, earliest-expiring balances, then deterministic date tie-break.
3. Run in a Web Worker with a hard time limit; report optimal, infeasible, or timed-out-with-incumbent distinctly.
4. Measure cold Wasm load, solve latency, memory, produced asset size, and Angular SSR/build integration. Check one intentionally contradictory obligation set and one case where ANY must preserve a typed balance for a later obligation.

Adopt only if representative inputs are optimal and deterministic in under five seconds on a recent mid-range phone, with a hard ten-second solve limit. Measure cold Wasm loading separately and lazy-load it when calculation is requested; if the spike fails, retain the dependency-free heuristic rather than moving to Z3.