# 技术路线图

本文件写里程碑、每个里程碑的**完成标准**、以及下一步的方向。里程碑只有在完成标准全部满足之后才算
结束，未达成时不允许把相应能力写进对外承诺。逐轮的实测过程与已否决的方案在 [`history.md`](history.md)。

## 里程碑总览

| 里程碑 | 主题 | 状态 |
| --- | --- | --- |
| M1 | 基础层与模型层：`core`、`model`、`oracle`、公开入口、CLI 与示例 | 已完成 |
| M2 | 标准模型输入：MPS（free / fixed）与 LP 格式读写 | 已完成 |
| M3 | 稀疏求解内核：修正单纯形 + 对偶单纯形 + presolve / postsolve | 完成标准已满足 |
| M4 | 证书与独立校验器：最优性、Farkas、无界射线 | 已完成 |
| M5 | 整数规划：分支定界 + 割平面 | 完成标准①②③全部满足 |
| M6 | 基准对拍、CLI、文档与发布 | 已完成（已发布 `0.1.0` / `0.1.1` / `0.1.2` / `0.2.0`） |

## M1 · 基础层与模型层

**交付物**：`core`（容差比较、Neumaier 补偿求和、CSC 稀疏矩阵）、`model`（变量、表达式、约束、目标、
校验）、`oracle`（稠密两阶段单纯形参考实现）、公开入口 `solve` / `solve_with` 与结果类型、
`cmd/main` 与两个可运行示例。

**完成标准（已满足）**：`moon check --deny-warn` 与 `moon test --deny-warn` 全绿；`moon fmt` / `moon info`
之后 `git diff --exit-code` 为空；native / wasm-gc / js 三个目标测试全绿；能力边界如实标注，越界调用
返回 `NotSolved` 加原因。

## M2 · 标准模型输入

**交付物**：`format` —— MPS（free / fixed）读取器与写出器、LP 格式读写、解析错误定位到行列号与具体
token；`cmd/parse` 巡检 CLI 与 `bench/` 的下载 / 报告脚本，让 `format` 能直接吃真实实例。

**完成标准（已满足）**：

- 读→写→读幂等：写出的文本再次写出逐字节相同；
- 真实实例解析：MIPLIB 2017 清单 32 个实例全部成功，见 [`../bench/parse-report.md`](../bench/parse-report.md)；
- 畸形输入只报错、不 panic，且错误信息带位置：`ParseIssue` 带行号、列号与 token，9 个畸形用例逐条断言
  位置与原因。

**被真实数据纠正过的两点**：额外的 `N` 行是 MPS 的 free row，系数应忽略而不是报错；真实文件里的
`1.5D+02` 指数写法、粘连表达式、`free` / `infinity` 写法都要显式支持。

## M3 · 稀疏求解内核

**交付物**：`simplex`（稀疏 CSC + 稀疏 LU 基分解 + 乘积形式基更新、有界变量枢轴、增益定价、
Harris 比值检验与 Bland 兜底、对偶单纯形热启动、证书生产端自检）、`presolve`（归约与还原）。

**完成标准（已满足）**：

- 与 `oracle` 参照实现在随机 LP 上差分一致；
- presolve / postsolve 在 150 个随机模型上与未化简路径一致，且还原解在**原模型**上复核通过；
- 基准报告可由脚本复现，见 [`../bench/solve-report.md`](../bench/solve-report.md)（32 个实例中 20 个求到
  最优、11 个超行数上限跳过、1 个到 20000 枢轴上限）。

**增强项（未做，见"下一步"）**：DeVex / steepest-edge 定价、更完整的 presolve 归约族。

## M4 · 证书与独立校验器

**交付物**：`verify` —— 独立于求解路径的最优性校验（原始可行性、对偶可行性、互补松弛、对偶间隙）、
Farkas 不可行射线、无界射线 + 可行起点、割的再推导、证书 JSON 序列化、CLI `verify` 子命令。

**完成标准（已满足）**：

- 故意注入的错解必须被拒，包括数值上"看起来对"的错解：覆盖"可行但非最优"、"偏离可行域一点点"、
  "看起来像但与点不配套的对偶"、目标值声称错、形状不对、符号错误的 Farkas 射线、零射线，
  以及对真实求解结果篡改后的三项；另有一条故意做错的求解器给出的答案必须被 `mip` 停下；
- 校验器不复用求解器的内部中间量：`verify/moon.pkg` 只 import `core`、`model` 与 `moonbitlang/core/string`，
  整包不含任何 `@simplex` 引用；
- 三类结论的证书都能被独立实现复核：200 个随机模型的语料上三种主张都出现且全部通过；真实实例上
  `flugpl` / `blend2` / `noswot` / `30n20b8` 的 `--verify` 全部 accepted（对偶间隙 ~1e-13）。

**限度**：Farkas 射线的构造仍是"Phase I 的最优对偶解"，不是显式导出的构造（生产端已按校验器的方式
自检三条测量）；无界射线只自检了"点可行"。

## M5 · 整数规划

**交付物**：`mip` —— best-bound 分支定界（节点 = 父节点 + 一条收紧的界，沿链重建，子节点热启动）、
根节点割（混合整数舍入，带推导证明）、原始启发式（取整读出整点、取整修复、可行性泵、下潜）、
cutoff 传播、预算合同。

**完成标准与实际结果**：

1. **小规模整数实例求到公开已知最优值：满足**。10 个实例 / 30000 节点的报告口径下 **5 个证到公开已知
   最优值**，对拍脚本 [`../bench/check-mip-objectives.ps1`](../bench/check-mip-objectives.ps1) 对 5 项
   **取等**通过；另外 5 个到节点预算（`markshare1` / `markshare2` / `pk1` 的界贴下界）。
   见 [`../bench/mip-report-small.md`](../bench/mip-report-small.md)。
2. **上限下给出过程状态：满足**，并由测试固定。节点预算到顶报 `NodeLimit`，同时给出当前整数点与仍在开
   的界；`markshare1` 在 20000 节点下给 61 / 下界 0，`pk1` 在 2000 节点下给不出整数点 / 下界 0.602，
   两者都没有被写成最优。
3. **每次 LP 重解都过 `verify`：满足**。报告的 `verified` 列是这件事的计数，另有"故意做错的节点求解器
   必须被拒"的测试；`verified < nodes` 的差额是"到达不了结论的松弛"，按开着的活计。

**覆盖面（宽口径）**：32 个实例 / 300 节点的报告口径下 3 个证到最优、12 个到节点预算、17 个超行数上限
跳过，见 [`../bench/mip-report.md`](../bench/mip-report.md)。未证的实例里，有 4 个跑完预算后界仍等于根
LP 松弛——瓶颈在松弛本身，不在搜索策略。

## M6 · 基准、CLI、文档与发布

**交付物**：四份基准报告 + 索引（含报告陈旧性的机械化判定）、CLI 的五个子命令与统一 JSON 输出、
设计 / 算法 / API / 路线图 / 生态调研文档、发布到 mooncakes.io。

**完成标准（已满足）**：

- 报告可由脚本一键复现，且脚本在运行没跑完、条目数不符、出现被拒证书、点没通过复核时**拒绝写报告**；
- 索引（[`../bench/report.md`](../bench/report.md)）对每份报告做陈旧性判决：读报告自己记的提交，
  把该报告依赖的源路径在那个提交与 HEAD 之间差分，有改动标 `STALE` 并列出文件；
- 发布版本通过 `moon check --deny-warn` / `moon test --deny-warn` 与全部目标平台测试；
  发布物自包含（归档解出来后当模块根 `moon check` / `moon test` 通过），且不含第三方数据。

## 下一步

按"难度 × 回报"排列，都属于研究性增量，不是工程欠账：

1. **扩大覆盖面**（回报最大）：宽口径 3/32、小规模 5/10。已知的堵点分别是 LP 松弛本身（有实例跑完
   预算后界仍等于根 LP）与证明成本（`fast0507` 在 20000 枢轴上限内跑不完）。
2. **更完整的整体 presolve / 归约族**（系数强化、对偶固定、行与列的支配检测）与 **DeVex / steepest-edge
   定价**：前者可能同时改善两个口径的界与枢轴数，后者需要逐实例对比之后才决定。
3. **补齐射线自检**：无界主张的两项（行不阻挡该方向、目标严格改善）目前只做了点可行；Farkas 射线从
   "Phase I 最优对偶解"改成显式构造。
4. **导出到公开证书标准（VIPR）**：真正的成本是要一套有理数算术子系统——本项目的证书是浮点加带容差的
   判据，有理化会把证书变成另一份主张，必须重新论证它成立。做法与三个问题的答案见
   [`prior-art.md`](prior-art.md)。
5. **整数无界性的证明**：需要整数射线，现在遇到松弛无界只报 `NotSolved` / `UnboundedRelaxation`。

## 明确不做（非目标）

以下内容在可预见的版本内不做，也不写进对外承诺：

- 非线性 / 凸优化（NLP）、半定规划；
- 随机规划与分解算法（Benders、Lagrangian 松弛）；
- 并行 / 多线程求解；
- 网络单纯形专用高速路径；
- MPS 的极小众扩展（完整 `MARKER` / `SOS` 语义）与 CPLEX LP 格式的全部扩展；
- Python / JS 绑定（保持纯 MoonBit、零 FFI）。

## 规模承诺的措辞

不写"目标万级约束 / 变量"这类话。对外只报告**实测**结果：以公开实例清单为参照，列出每个实例的状态、
目标值、枢轴数或节点数，以及没解完的原因。任何"上限"都是结果的一部分，必须与它对应的数字一起给出。