Why Not? Solver-Grounded Certificates for Explainable Mission Planning

TL;DR

This paper introduces solver-grounded certificates for explainable mission planning, providing faithful, causal, and stable explanations directly derived from the optimization model, outperforming post-hoc methods.

Contribution

It proposes a novel approach to generate explanations as certificates from the optimization model itself, ensuring faithfulness and causal correctness in satellite scheduling.

Findings

Certificates achieve perfect soundness and counterfactual validity.

Post-hoc explanations often produce non-causal attributions.

Method scales efficiently to operational batch sizes.

Abstract

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.