MBOP-MAPF 尾段残余：单页读本

一个问题的全部证据链 · 最后更新 2026-11-09 · 给外部审计 Agent 阅读

问题：N=150 的多智能体路径规划里，样本级未解率 0.3225。这些未解，是「本来就没有解」，还是「我们的求解器走错了」？

下面每一节都能独立读。数字都带 n 与口径；有争议的结论单独标出来。凡是我们自己推翻自己的地方，都写在「修正」里，不删。

0 一句话答案

残余主要是「协调规则」的失败，不是搜索深度或空间不足。 状态在最后 3–7 步之前还有合法计划；失败发生在 1–6 个 agent 的联合动作上，而且 26/27 都涉及一个正站在自己目标格上的 agent。

0.369

25 景、141 个可判定样本里 t0 已死的比例（52 个，带证明）

0.846

6 景 52 个样本里，t0 或前 7 步内还有合法计划的比例

3.85

失败那一步的差异 agent 数（均值，150 个里）

26/27

差异集合里含一个 gd=0（已到家）的 agent

1 五层链条

1.1 现象：不是「到不了」，是「停不住」

样本级未解            0.3225（25 景 × 500）
moving 类到过家       143/167 = 0.856        （RESULT_T1）
到站后被带走          554,586 次离开全有放行  （RESULT_GOALHOLD_LEAVE）
互斥四格              (a) 0.988 / (b) 0.012

所以失败形态是：回到家 → 被挤走 → 再也回不去。

1.2 闸门：承重的是让位，不是冻结

GH_YIELD=0（没有解钉通道）   solved 0.497 -> 0.000（10 景，anchor=1）
ADJ（只对贴身挡路者让位）    +5.91pp  [+3.84, +7.69]
ADJPT（再加 post-freeze）    +11.69pp
唯一写回闸门                 main.py:2252

让位是承重的；让位过量是净负的。承重变量是「让给谁、让到哪」。

1.3 存在性：t0 的死是真的（全模型证明）

早期结论用了一个冻结模型（半径 2 外的 agent 当墙）。实测：52 个样本里只有 10 个被冻的 agent 全部在目标格上，中位 2 个其实还没到家。所以那个模型既不是松弛也不是限制。重做：

全模型完备 CBS（150 个都能动，全员必须回到自己目标格）
  34 证明不可行   0.654
  17 证明可解     0.327   （计划都过 check_solution，无 violation）
   1 未判定       0.019   （20 万节点仍 UNKNOWN）

两个翻转说明冻结模型有假阴性：scen 25/m14（19 节点）、scen 9/m0（102 节点）。

1.4 总体：死率不是一个数

25 景、141 个可判定样本（剔除 3 个 horizon 封顶的时间不足样本）
  证明不可行  52   0.369
  证明可解    87   0.617
  未判定       2   0.014

17/25 个景死数为 0；52 个死全部落在 8 个景里
同过滤：6 个硬景 0.643，其余 19 景 0.188

任何单一比例都会掩盖这一点。论文里必须分簇写。

1.5 时点：死是走出来的

34 个死状态，用 20 万节点逐步往前问同一个完备求解器
  27 个（0.79）在 t0−d 仍可解，d = 1..7（1:5 2:3 3:5 4:2 5:4 6:6 7:2）
   7 个（0.21）在 20 万节点下仍未判定
=> 52 个里 44 个（0.846）在 t0 或前 7 步内还有合法计划

修正：首版写「18 个在 t0−1 起就已证明不可行」，那是 2 万节点造成的假象；加预算后 13 个翻转。

1.6 机制：不是「看不到未来」

在最后一个可解时刻 t0−d 上，拿一个已验证计划的第一步，和求解器实际走的那一步逐 agent 对账：

差异 agent 数        1–6，均值 3.85（150 个里）
涉及 gd=0 的 agent   26/27
按差异集合的 gd 总和  计划更好 16 / 持平 6 / 更差 5

主因不是前瞻（只有 5 个），而是正确答案在距离上更近、求解器却没选它（16 个）。

这一步还没做完：差异 ≠ 致命。正在测「只翻一个 agent 的首步能否救活」—— 若能，失败是一个动作；若不能，才是至少两个的联合错误。

2 已经关掉的（不要再开）

方向	否掉它的数字
终点不可达	35/36 目标静态可达
合作集不够大	半径 2→4，44 个样本只变 1 个
2-环是死锁主因	21/36 死样本在 t0 完全没有环
环旋转能修	定理 (b)：SEQ=1 下循环位移 0 次；D5 无闸 valid=0/500，加闸后与基线逐位相同
静态必经格规则	会挡掉 0.38–0.51 的钉住，与 GH_YIELD=0 同构
动态割点规则	约 7.7e8 次操作/格，本机不可行
图不变量 / 局部拥挤	669 空位、1 连通分量、0 割点阻断、0 闭合口袋；局部空位死/活完全重叠
反向（终点当 agent）	时间反演是等价变换；数据是「进去了又出来」

3 还站着的

障碍是时间的，不是空间的。82% 的格子是空的（669/819，n=52 状态），图上没有信号。
交互集只有 1–6 个（均值 3.85）→ 联合值函数只需要在小集合上联合，不是 150 维。
失败分三类：16/27 正确答案距离更近却没被选中；5/27 需要前瞻；6/27 距离无差别。
末段完备求解的上限：最多救回 17/68 = 0.25 的未解样本（6 景内）。
死率分两簇：硬景 0.643 / 其余 0.188。

4 每轮交互记录

审计方的意见只记「它指出了什么、我们改了什么」，不记措辞。

轮	对象	它的结论	我们的动作
R1	CNB	3 处（写回清单、0.677 口径、§4 景集）	认 2 改 1 反证（t2_frames 含 12）
R2	CNB	883 是 S4 循环内的写回，不是首行	认，改 §3 与清单；2089 标为边界检查
R3	CNB	§1.6 行号表、2199b4b1 笔误、§3.1 可加性	行号表是反证（已在 234b8d6）；另两条认
R4	CNB	taken 有两个定义	反证：同一变量，代码行给出；CNB 下一轮撤回
R5	CNB	§3.1:161「冻结后位置」与口径句互斥	认，改成「写回之后的 t+1 实际占格」
GH1–3	Notion	桥接证据一格 vs 10 格	认，改为「一格」，归因降为有条件
GH4	Notion	(c) 三个 0 节点不可行	真的：horizon 封顶导致时间不足；死率 0.382 → 0.369

5 怎么复核

# 全模型 CBS 的 6 条用例（含负向：无口袋必须证明不可行、预算 0 必须 UNKNOWN）
python -m pytest experiments/yieldback_2026-10-17/ledger/test_cbs_full.py -q

# 存在性：34 / 17 / 1
python -u experiments/yieldback_2026-10-17/ledger/probe_tail_full_cbs_2026-11-09.py

# 总体：52 / 87 / 2 over 141
python -u experiments/yieldback_2026-10-17/ledger/probe_tail_25_2026-11-09.py

# 时点：27 个可退步，d 分布
python -u experiments/yieldback_2026-10-17/ledger/probe_tail_backward_2026-11-09.py

# 机制：27 个逐 agent 对账
python -u experiments/yieldback_2026-10-17/ledger/probe_tail_mechanism_2026-11-09.py

6 文件索引

存在性   RESULT_TAIL_EXACT_2026-11-09.md / cbs_full.py
总体     RESULT_TAIL_25_2026-11-09.md
时点     RESULT_TAIL_BACKWARD_2026-11-09.md
机制     RESULT_TAIL_MECHANISM_2026-11-09.md
闸门     RESULT_GOALHOLD_LEAVE_2026-11-08.md / RESULT_GH0_QUICK_2026-11-08.md
规则     RESULT_PIN_RULE_FEASIBILITY_2026-11-09.md / PREREG_PIN_CUT_2026-11-09.md
定理     THEOREM_DEADLOCK_2026-11-08.md
总账     STATUS_TAIL_2026-11-09.md