# 设计说明

## 目标

把 MoonBit 的 LP/MILP 做成一个能与工业数据和公开基准对拍的求解内核。设计只服务三件事：

1. **互通**：能吃行业标准的模型文件（MPS / LP），所以结果可以和外部工具、公开数据集对拍。
2. **规模**：稀疏存储 + 修正单纯形 + presolve，而不是整张稠密 tableau。
3. **可信**：解与证书一起产出，证书可被独立校验；数值不可靠时**报失败**，不静默给错解。

不做的事见 [`roadmap.md`](roadmap.md) 的"明确不做"。

## 包边界

```
core      数值与稀疏基础设施。不依赖本模块其它包。
model     LP/MILP 模型层（变量、表达式、约束、目标、校验）。依赖 core。
oracle    稠密两阶段单纯形，仅作差分测试的对照基准。依赖 core、model。
format    MPS/LP 读写。依赖 core、model。
simplex   稀疏修正单纯形与对偶单纯形，含证书的生产端自检。依赖 core、model。
presolve  presolve / postsolve。依赖 core、model。
verify    证书校验与割的再推导。依赖 core、model。
mip       分支定界与割平面。依赖 simplex、verify。
moonopt   根包：对外的 solve / solve_with 与结果类型，只做编排。
```

规则：**算法细节只出现在被它服务的包里**，根包保持薄；包之间只经由 `.mbti` 公开接口通信。
`verify` 不依赖 `simplex`，这是"证书"这个词的意义所在——校验器与求解器不共享任何状态，
`verify/moon.pkg` 就是这条约束的可检查形式。

## 数据表示

- 稀疏矩阵用 **CSC**（`col_ptr` / `row_idx` / `values`）：列内行号升序、不存结构零。
  修正单纯形以列为主做定价与基更新，所以按列存。
- 累加走 `core` 的 Neumaier 补偿求和，禁止裸 `+=` 累加大规模求和。
- 变量界是 `Var.lb` / `Var.ub`，用 `±1e30` 量级的哨兵表示数值意义上的无界
  （有界变量枢轴需要一个可比大小的界；IEEE 无穷会让比值检验退化）。
- 列里存 `(变量下标, 系数)` 对，构造时排序、合并同类项、丢掉精确零，保证同一模型的不同写法归一。

## 数值策略

| 关注点 | 策略 |
| --- | --- |
| 零判定 | 统一用 `core` 的容差助手，禁止用 `==` 比较浮点 |
| 误差累积 | 补偿求和；不复用已经污染的中间量 |
| 退化的基 | 确定性退化扰动（默认 `1e-12`）打破平局；自检与答案门禁一律按未扰动的右端项测量 |
| 比值检验 | Harris 两遍法 + 可行性守卫；停滞时切 Bland 规则保证终止 |
| 基稳定性 | 稀疏 LU + 乘积形式（eta）更新，周期性重新分解；填充量由预算约束 |
| 结论自检 | 每个结论都要量它所依赖的那个方程的残差（详见 [`algorithms.md`](algorithms.md#2-修正单纯形内核)） |
| 失败处理 | 迭代上限、数值失败、超出规模边界都返回 `NotSolved` 并带原因，绝不返回可疑解 |

## 证书

- **最优性**：原始解 `x` + 满足符号约定的行乘子 `y` + 互补松弛 + 对偶间隙为零。
- **不可行性**：Farkas 射线，同一套式子取 `c = 0` 并要求严格为正。
- **无界性**：一个可行起点加一条改善射线。

推导写在 `verify/verify.mbt` 的包文档里。内核产出的证书与 `verify` 的判据共用同一套尺度，
否则会变成"生产者与被评判者量不同的东西"；这一条在 [`algorithms.md`](algorithms.md) 与
[`api.md`](api.md) 都有展开。

## 差分测试

`oracle` 只有一个用途：给 `simplex` 一个未优化、易读的参照实现做差分测试。它是**参考实现而不是
交付求解器**，能力边界（稠密、规模小）写在它自己的文档里。随机 LP 生成器 + `oracle` + `simplex`
三方对拍，是内核正确性的主要手段之一（另一条是与 `verify` 的证书闭环）。

## 能力边界怎么对使用者呈现

- `README.md` 用一张表写"支持 / 暂不支持"，暂不支持的每一项都对应一条返回 `NotSolved` 并带原因的代码路径；
- `moon run cmd/main` 里保留一个"当前不支持"的诚实用例，让边界可见而不是靠读源码发现；
- 任何新增能力都要同时更新那张表与 `CHANGELOG.md`。