# Why Not? Solver-Grounded Certificates for Explainable Mission Planning

arXiv: https://arxiv.org/abs/2603.00469 · HTML: https://mlsanity.com/paper/2603.00469/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 16 references that are in the map.
- First posted on arXiv 28 Feb 2026.

## Builds on (most cited first, 2 of 2)

- [A framework for step-wise explaining how to solve constraint satisfaction problems](https://mlsanity.com/paper/2006.06343/) (2020)
- [Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)](https://mlsanity.com/paper/2303.11712/) (2023)

## Built on by (most cited first, 1 of 1)

- [A property-registry contract for retrieve-or-refuse thermal-mechanical lattice search](https://mlsanity.com/paper/2609.14741/) (2026)

## Abstract (arXiv)

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.