From ba8dbe92d953af4528e8bcafad6def95033f7849 Mon Sep 17 00:00:00 2001
From: Nessar
Date: Fri, 28 Aug 2026 17:00:12 +0200
Subject: [PATCH] feat: enhance documentation for leave planning concepts and
solver recommendations
---
CONTEXT.md | 79 ++++++++++++++++---
.../0001-ordered-heuristic-optimization.md | 2 +
...constraint-first-lexicographic-planning.md | 3 +
docs/research/leave-planning-solver.md | 74 +++++++++++++++++
4 files changed, 147 insertions(+), 11 deletions(-)
create mode 100644 docs/adr/0003-constraint-first-lexicographic-planning.md
create mode 100644 docs/research/leave-planning-solver.md
diff --git a/CONTEXT.md b/CONTEXT.md
index 11d3dab..4faf7f8 100644
--- a/CONTEXT.md
+++ b/CONTEXT.md
@@ -5,18 +5,30 @@ VacOptimizer helps one person turn expiring leave balances into a leave plan acr
## Language
**Leave entitlement**:
-Leave made available to the person by a company or generated by an applicable planning rule.
+A quantity of leave granted by a company or generated by an applicable planning rule, with an availability date and an expiry date.
**Leave balance**:
-The currently available, unspent quantity of a leave entitlement, identified by leave type and expiry date.
+The unspent quantity of a leave entitlement, identified by leave type, availability date, and expiry date.
_Avoid_: vacation day, VacDay
+**At-risk balance**:
+A leave balance whose expiry date falls between the planning horizon's start and end, including both boundary dates. Its unplaced quantity is at risk of being lost.
+
+**Unavoidable expiry**:
+Leave whose expiry date precedes the planning horizon and therefore cannot be saved by that plan.
+
+**Deferred balance**:
+The unspent portion of a leave balance that expires after the planning horizon. It needs no ordinary placement in the current plan but remains available to explicit planning rules and supporting placements.
+
**Leave type**:
The category of leave in a balance: CP (paid leave), RTT (working-time reduction leave), or Other (a user-managed catch-all).
_Avoid_: ANY as a leave type; `ANY` is only a rule selector.
**Planning horizon**:
-The period beginning today over which a plan is generated. The current horizon is a rolling 12 months.
+The user-selected half-open date interval of at most 12 months within which leave may be placed. It defaults to today's Europe/Paris calendar date through the same date 12 months later.
+
+**Working day**:
+A Monday-to-Friday calendar date that is not a French national public holiday. Only working days can receive leave placements.
**Public holiday**:
A French calendar date that cannot receive a leave placement and contributes to a time-off period.
@@ -24,27 +36,72 @@ A French calendar date that cannot receive a leave placement and contributes to
**Leave placement**:
Using one or more working days from a leave balance on specific dates within the planning horizon.
+**Supporting placement**:
+A leave placement from a deferred balance that captures additional adjacent non-working dates, eliminates a short work sequence, or reduces the longest work sequence. Merely extending an existing period by the placed day itself is not sufficient.
+
**Time-off period**:
-A contiguous period created by combining leave placements with weekends and public holidays.
+A contiguous period containing at least one leave placement together with any adjacent weekends and public holidays, including those immediately outside the planning horizon.
+
+**Time-off duration**:
+The number of distinct calendar dates covered by all planned time-off periods.
+
+**Non-working-day gain**:
+The distinct weekend and public-holiday dates contained in planned time-off periods. Leave placement dates themselves do not contribute to this gain.
+
+**Work sequence**:
+The working days in an interval delimited by planned time-off periods or by the planning horizon edges. Intervening weekends and public holidays neither count nor split the sequence.
+
+**Short work sequence**:
+A work sequence of fewer than five working days between two planned time-off periods.
**Planning rule**:
-An ordered user preference that requests leave placements around a calendar opportunity or inside a date window.
+A user instruction that requests leave placements around a calendar opportunity or inside a date window. Its force is either an obligation or a preference.
+
+**Obligation rule**:
+A planning rule that every valid plan must satisfy. Obligation rules are resolved jointly; their order only breaks ties between valid plans.
+
+**Preference rule**:
+A planning rule that guides placement but may remain unsatisfied to preserve validity or prevent more at-risk leave from expiring.
**IF_THEN rule**:
-A planning rule triggered when a French public holiday falls on its configured weekday. It places a complete requested pattern before, after, or around that holiday; if the pattern cannot be satisfied, the rule is skipped.
+A planning rule evaluated independently for every French public holiday on its configured weekday. A preference requests a complete pattern around each occurrence when possible; an obligation requires it for every occurrence.
+
+**IF_THEN placement mode**:
+`before` and `after` fix every requested day on one side; `around` considers every split with at least one day on each side; `auto` considers every split, including the all-before and all-after extremes.
**TIME_WINDOW rule**:
-A planning rule that places up to its requested number of leave days on working days within an inclusive date window.
+A planning rule targeting working days in an inclusive date window. A preference requests up to its configured quantity; an obligation requires exactly that quantity.
**Rule priority**:
-The order in which planning rules are applied. Earlier rules reserve their placements and consume available balances before later rules; the optimizer does not backtrack.
+The user-defined lexicographic order of preference rules. Each earlier preference is satisfied as far as possible before a later preference is considered.
+
+**Rule satisfaction**:
+The relationship in which a plan fulfils a planning rule. One compatible leave placement may contribute to the satisfaction of multiple rules.
+
+**Placement provenance**:
+The consumed leave entitlement and every planning rule satisfied by a leave placement.
+
+**Planning conflict**:
+A set of obligation rules that cannot all be satisfied by one plan within the planning horizon and available leave balances.
+
+**Invalid planning input**:
+A malformed request that cannot describe a plan, such as a reversed date window. A valid but unsatisfiable request is a planning conflict instead.
+
+**Planning outcome**:
+The result of a calculation: invalid input, a planning conflict, an optimization result, or an incomplete calculation.
+
+**Incomplete calculation**:
+A calculation stopped before it completed the planning objective order. It may expose its best valid plan but never implies that the obligations conflict.
+
+**Planning objective order**:
+The lexicographic quality order applied after joint obligation feasibility: minimize unplaced at-risk leave; satisfy each preference in user order; maximize non-working-day gain; minimize the longest work sequence; minimize the total deficit of internal work sequences shorter than five days; minimize supporting placements; consume earlier-expiring balances; then prefer earlier placement dates. A lower criterion never degrades a higher one.
**Earned leave entitlement**:
-A new leave entitlement created by a planning rule as a consequence of a placement. It may be used by later rules and by ordinary placement in the same plan.
+A leave entitlement created for each completed occurrence of an applicable planning rule after its generating time-off period ends. It becomes available the following day, expires one year later, and may fund any later compatible placement.
_Avoid_: reward, bonus days
**Optimization result**:
-One deterministic plan produced from the original balances and enabled rules. It favors useful adjacent time-off periods but does not promise a mathematically globally optimal result.
+A valid deterministic plan produced after completing the planning objective order, containing leave placements and their provenance, time-off periods, unsatisfied preference reasons, and remaining balances with reasons. It does not claim mathematical global optimality.
**Remaining balance**:
-The portion of a leave balance that the optimization result did not place.
+Any quantity left unspent by the optimization result, reported as unavoidable expiry, an unplaced at-risk balance, or a deferred balance.
diff --git a/docs/adr/0001-ordered-heuristic-optimization.md b/docs/adr/0001-ordered-heuristic-optimization.md
index 13606b8..45251a1 100644
--- a/docs/adr/0001-ordered-heuristic-optimization.md
+++ b/docs/adr/0001-ordered-heuristic-optimization.md
@@ -1,3 +1,5 @@
# Ordered Heuristic Optimization
+Superseded by [ADR 0003](0003-constraint-first-lexicographic-planning.md).
+
VacOptimizer applies enabled planning rules in user-defined order and then uses a deterministic heuristic to choose placements; it does not backtrack or promise a globally optimal plan. This keeps results predictable and fast for the personal planner while leaving room to improve the heuristic later.
diff --git a/docs/adr/0003-constraint-first-lexicographic-planning.md b/docs/adr/0003-constraint-first-lexicographic-planning.md
new file mode 100644
index 0000000..27a0e44
--- /dev/null
+++ b/docs/adr/0003-constraint-first-lexicographic-planning.md
@@ -0,0 +1,3 @@
+# Constraint-First Lexicographic Planning Without a Solver Dependency
+
+VacOptimizer resolves obligation rules exactly and jointly, then applies deterministic heuristic stages for at-risk loss, ordered preferences, calendar gain, work-sequence quality, supporting placements, balance expiry, and dates in that order; a completed plan does not claim mathematical global optimality. The dependency-free planner targets five seconds, returns `PlanningIncomplete` if those stages are interrupted, and stops after ten seconds. A HiGHS WebAssembly spike missed that hard limit on representative inputs even on the development machine, so no solver dependency is accepted. This supersedes ADR 0001.
diff --git a/docs/research/leave-planning-solver.md b/docs/research/leave-planning-solver.md
new file mode 100644
index 0000000..6f2c869
--- /dev/null
+++ b/docs/research/leave-planning-solver.md
@@ -0,0 +1,74 @@
+# 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.