Why Not? Solver-Grounded Certificates for Explainable Mission Planning

Najeeb Khan

cs.AIFeb 28, 2026

Why Not? Solver-Grounded Certificates for Explainable Mission Planning

Authors: Najeeb Khan

Organizations: Serana AI Inc., Vancouver, Canada

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.

Figures & tables

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.

Intrinsic correctness
Infeasibility certificates	7
Soundness checks passed	15 / 15
Counterfactual tests succeeded	7 / 7
Stability (Jaccard, 28 seed-pairs)	1.000
Core size (avg / median / max)	2.1 / 2.0 / 3
Post-hoc baseline failure modes

Table 1: Evaluation results. All metrics are over the 7 constraint-infeasible orders unless noted. Top: intrinsic correctness. Bottom: post-hoc baseline failure modes (certificate output as ground truth).

Operational (query-time)
Component	Time
Scheduling solve (CP-SAT)	6 ms
Certificate extraction (MIS)	440 ms
Offline validation
Soundness verification	64 ms
Counterfactual testing	1 197 ms

Table 2: Wall-clock timing breakdown for the test instance (3 satellites, 1 ground station, 10 orders, Apple M4 CPU).

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).

Counterfactual Explanations

Counterfactual explanations show how changing an input could alter a model’s prediction, supporting model understanding, auditing, and actionable recourse.

See all 109 papers

Optimizing Earth Observation Satellite Schedules under Unknown Operational Constraints: An Active Constraint Acquisition Approach
Apr 14, 2026Mohamed-Bachir BelaidConstrained Optimization Learning to Optimize
NILU, Climate and environmental research institute, Kjeller, Norway
Constraint-Anchored Attribution: Feasibility-Certified Counterfactuals and Bonferroni-PAC Sufficient Subsets for Neural CO Policies
May 24, 2026Sohaib LafifiFeature Attribution Counterfactual Explanations
Univ. Artois, UR 3926, Laboratoire de Génie Informatique et d’Automatique de l’Artois (LGI2A) Béthune, France
FCx: An algorithm for finding Feasible Counterfactual Explanations
Sep 16, 2026Kleopatra Markou, Vana Kalogeraki, Dimitrios GunopulosCounterfactual Explanations
National and Kapodistrian University of Athens, Department of Informatics and Telecommunications, Greece · Athens University of Economics and Business, Department of Informatics, Greece

Apr 14, 2026J/K move · Enter open · S save

Optimizing Earth Observation Satellite Schedules under Unknown Operational Constraints: An Active Constraint Acquisition Approach

Mohamed-Bachir Belaid

NILU, Climate and environmental research institute, Kjeller, Norway

Constrained Optimization Learning to Optimize Remote Sensing

Open paper AskPDF arXiv

Earth Observation (EO) satellite scheduling (deciding which imaging tasks to perform and when) is a well-studied combinatorial optimization problem. Existing methods typically assume that the operational constraint model is fully specified in advance. In practice, however, constraints governing separation between observations, power budgets, and thermal limits are often embedded in engineering artefacts or high-fidelity simulators rather than in explicit mathematical models. We study EO scheduling under unknown constraints: the objective is known, but feasibility must be learned interactively from a binary oracle. Working with a simplified model restricted to pairwise separation and global capacity constraints, we introduce Conservative Constraint Acquisition~(CCA), a domain-specific procedure designed to identify justified constraints efficiently in practice while limiting unnecessary tightening of the learned model. Embedded in the Learn&Optimize framework, CCA supports an interactive search process that alternates optimization under a learned constraint model with targeted oracle queries. On synthetic instances with up to 50tasks and dense constraint networks, L&O improves over a no-knowledge greedy baseline and uses far fewer main oracle queries than a two-phase acquire-then-solve baseline (FAO). For $n\leq 30$ , the average gap drops from 65--68% (Priority Greedy) to 17.7--35.8% using L&O. At $n{=}50$ , where the CP-SAT reference is the best feasible solution found in 120s, L&O improves on FAO on average (17.9% vs.\ 20.3%) while using 21.3 main queries instead of 100 and about

5\times

less execution time.

Abstract

Counterfactual Explanations

Explore similar work

Optimizing Earth Observation Satellite Schedules under Unknown Operational Constraints: An Active Constraint Acquisition Approach

Constraint-Anchored Attribution: Feasibility-Certified Counterfactuals and Bonferroni-PAC Sufficient Subsets for Neural CO Policies

FCx: An algorithm for finding Feasible Counterfactual Explanations