Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Why Not? Solver-Grounded Certificates for Explainable Mission Planning

Najeeb Khan

TL;DR

This work takes 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.

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.

Why Not? Solver-Grounded Certificates for Explainable Mission Planning

TL;DR

This work takes 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.

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.
Paper Structure (38 sections, 7 equations, 4 figures, 2 tables)

This paper contains 38 sections, 7 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Problem Formulation
  4. Integrated EO Scheduling
  5. Decision variables.
  6. Objective function.
  7. Assignment constraints.
  8. Downlink requirement.
  9. Temporal exclusion.
  10. Storage reservoir.
  11. Feasibility filters.
  12. Semantic Constraint Tags
  13. Faithfulness Requirements
  14. Proposed Approach
  15. Challenges with Post-hoc Explanation Layers
  16. ...and 23 more sections

Figures (4)

  • Figure 1: Explanation pipeline. An operator query triggers model augmentation and certificate extraction (MIS for why-not, contrastive analysis for why, inverse solve for what-if). Semantic tags map solver constraints to operator categories. Offline verification (dashed) is not required at query time.
  • Figure 2: Conjunction failure mode. An order's candidates span two satellite types, each blocked by a different constraint kind. The certificate identifies both as jointly necessary; the baseline reports only the single best candidate's cause.
  • Figure 3: Operational latency vs. order count (10 satellites, 5 ground stations). MIS extraction dominates total latency; the CP-SAT solve remains negligible ($<$210 ms) across all tested sizes.
  • Figure 4: Constellation scaling (50 orders, 5 ground stations). Per-certificate cost increases with constellation size, but total latency remains bounded because more orders become schedulable, reducing the number of certificates needed (bars).