Why Not? Solver-Grounded Certificates for Explainable Mission Planning
This addresses the need for trustworthy explanations in mission planning for satellite operators, offering a novel approach over incremental post-hoc methods.
The paper tackled the problem of providing justifications for satellite scheduling decisions by deriving certificates directly from the optimization model, achieving perfect soundness, counterfactual validity, and stability in tests, while a baseline had non-causal attributions in 29% of cases.
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.