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](https://ergo-code.github.io/HiGHS/stable/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](https://github.com/lovasoa/highs-js), [npm package](https://www.npmjs.com/package/highs)). HiGHS and the wrapper are MIT-licensed ([HiGHS source](https://github.com/ERGO-Code/HiGHS), [`highs` registry metadata](https://registry.npmjs.org/highs/1.15.2)). 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](https://ergo-code.github.io/HiGHS/stable/structures/enums/)). Its core supports prioritized lexicographic linear objectives when `blend_multi_objectives` is false ([multi-objective optimization](https://ergo-code.github.io/HiGHS/stable/guide/further/)). 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`](https://ergo-code.github.io/HiGHS/stable/structures/classes/HighsIis/)), and the current wrapper repository documents `getIis` in its persistent API ([highs-js API map](https://github.com/lovasoa/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](https://github.com/lovasoa/highs-js/blob/main/README.md)) | Native prioritized linear objectives in HiGHS; sequential exact integer objectives are a fallback ([HiGHS guide](https://ergo-code.github.io/HiGHS/stable/guide/further/)) | MIT; `highs` 1.15.2; 3,525,070 bytes unpacked ([registry metadata](https://registry.npmjs.org/highs/1.15.2)) | 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](https://github.com/Z3Prover/z3/blob/master/src/api/js/PUBLISHED_README.md)) | `Optimize` defaults to objective declaration order ([Z3 guide](https://microsoft.github.io/z3guide/docs/optimization/combiningobjectives/)) | MIT; `z3-solver` 5.2.0; 35,820,846 bytes unpacked ([registry metadata](https://registry.npmjs.org/z3-solver/5.2.0)) | 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](https://github.com/MiniZinc/minizinc-js#readme)) | 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](https://github.com/MiniZinc/minizinc-js), [registry metadata](https://registry.npmjs.org/minizinc/4.5.1)) | 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](https://developers.google.com/optimization/install/)) | Strong semantic fit for Boolean/integer scheduling; integer-only constraints and objectives ([CP-SAT guide](https://developers.google.com/optimization/cp/cp_solver)) | Apache-2.0 and actively released ([repository](https://github.com/google/or-tools), [releases](https://github.com/google/or-tools/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](https://github.com/jvail/glpk.js/)) | Published API exposes one linear objective; exact priority therefore needs repeated solves ([API](https://github.com/jvail/glpk.js/#api)) | GPL-3.0; 2,616,261 bytes unpacked for 5.0.0 ([registry metadata](https://registry.npmjs.org/glpk.js/5.0.0)) | Reject; no material advantage over MIT HiGHS |
| **Choco Solver** | Java library distributed through Maven; no official TS/browser binding ([project repository](https://github.com/chocoteam/choco-solver)) | Constraint programming is a semantic fit | BSD-3-Clause and recently maintained ([project repository](https://github.com/chocoteam/choco-solver)) | Reject for this architecture |
| **Timefold Solver** | Official open-source solver targets Java and Kotlin, with JVM/Maven setup ([project repository](https://github.com/TimefoldAI/timefold-solver), [quickstarts](https://docs.timefold.ai/timefold-solver/1.x/quickstart/overview)) | 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](https://github.com/timefoldai/timefold-solver)) | 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](https://github.com/Z3Prover/z3/blob/master/src/api/js/PUBLISHED_README.md#limitations)). At 35.8 MB unpacked it is also roughly ten times the installed size of `highs` ([registry metadata](https://registry.npmjs.org/z3-solver/5.2.0)). 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.