为卫星调度提供可信赖的解释，确保每条理由都源自优化模型本身。
Why Not? Solver-Grounded Certificates for Explainable Mission Planning
- 解释来自优化模型的证书，而非事后拼凑
- 在15个约束检查中全部正确，7个反事实验证全通过
- 适合需要高可信度解释的航天任务规划场景
地球观测卫星操作员需要调度决策的合理解释：为何请求被选中、拒绝，或如何调整才能可行。现有方法依赖独立于优化器的事后推理层，存在非因果归因、约束组合遗漏和求解路径依赖问题。本文提出以忠实性为先的方法：每个解释都是从优化模型中直接生成的证书——拒绝时为最小不可行子集，选择时为紧约束与对比权衡，查询时为逆向求解。在具有结构差异约束交互的调度实例上，证书在15个引用约束检查中达到完美保真（15/15），反事实有效性7/7，稳定性（Jaccard = 1.0）在28组种子对中一致；而事后基线在29%情况下产生非因果归因，且所有多因拒绝均遗漏约束组合。扩展性分析表明，最多支持200个订单和30颗卫星，实际提取时间满足运行批次需求。
原文摘要 · Abstract (English)
Operators of Earth observation satellites need justifications for scheduling decisions: why a request was selected, rejected, or what changes would make it schedulable. Existing approaches construct post-hoc reasoning layers independent of the optimizer, risking non-causal attributions, incomplete constraint conjunctions, and solver-path dependence. We take a faithfulness-first approach: every explanation is a certificate derived from the optimization model itself: minimal infeasible subsets for rejections, tight constraints and contrastive trade-offs for selections, and inverse solves for what-if queries. On a scheduling instance with structurally distinct constraint interactions, certificates achieve perfect soundness with respect to the solver's constraint model (15/15 cited-constraint checks), counterfactual validity (7/7), and stability (Jaccard = 1.0 across 28 seed-pairs), while a post-hoc baseline produces non-causal attributions in 29% of cases and misses constraint conjunctions in every multi-cause rejection. A scalability analysis up to 200 orders and 30 satellites confirms practical extraction times for operational batches.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。