Why Not? Solver-Grounded Certificates for Explainable Mission Planning
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Why Couldn't You do that? Explaining Unsolvability of Classical Planning Problems in the Presence of Plan Advice
Explainable planning is widely accepted as a prerequisite for autonomous agents to successfully work with humans. While there has been a lot of research on generating explanations of solutions to planning problems, expla…
Emission-Aware Optimization of Gas Networks: Input-Convex Neural Network Approach
Gas network planning optimization under emission constraints prioritizes gas supply with the least CO$_2$ intensity. As this problem includes complex physical laws of gas flow, standard optimization solvers cannot guaran…
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that refor…
Dsat: A Native SAT Solver for Discrete Logic
Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for …
Embodied CAD: Solver-Grounded LLM Agents for Parametric B-Rep Assembly Modeling
Large language models can write plausible CAD scripts, but reliable industrial CAD modeling requires more than syntactically valid code: every feature, placement, and assembly relation must be accepted by an exact geomet…