# Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 82 references that are in the map.
- First posted on arXiv 21 Mar 2023.

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

- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- [Explanation in Artificial Intelligence: Insights from the Social Sciences](https://mlsanity.com/paper/1706.07269/) (2017)
- [A Survey Of Methods For Explaining Black Box Models](https://mlsanity.com/paper/1802.01933/) (2018)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [A Survey on Computational Propaganda Detection](https://mlsanity.com/paper/2007.08024/) (2020)
- [Explainable Planning](https://mlsanity.com/paper/1709.10256/) (2017)
- [A framework for step-wise explaining how to solve constraint satisfaction problems](https://mlsanity.com/paper/2006.06343/) (2020)
- [Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)](https://mlsanity.com/paper/2104.13138/) (2021)

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

- [Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach](https://mlsanity.com/paper/2508.07015/) (2025)
- [Why Not? Solver-Grounded Certificates for Explainable Mission Planning](https://mlsanity.com/paper/2603.00469/) (2026)
- [Exploiting Symmetries in MUS Computation (Extended version)](https://mlsanity.com/paper/2412.13606/) (2024)
- [Exploiting Constraint Reasoning to Build Graphical Explanations for Mixed-Integer Linear Programming](https://mlsanity.com/paper/2507.13007/) (2025)
- [Exploring Plan Space through Conversation: An Agentic Framework for LLM-Mediated Explanations in Planning](https://mlsanity.com/paper/2603.02070/) (2026)

## Abstract (arXiv)

We build on a recently proposed method for stepwise explaining solutions of Constraint Satisfaction Problems (CSP) in a human-understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified using a cost function. The algorithms for explanation generation rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant explanations and MUSs. However, MUS extraction algorithms do not provide any guarantee of subset minimality or optimality with respect to a given cost function. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to generate explanations efficiently that are provably optimal (with respect to the given cost metric). For that, we developed (1) a hitting set-based algorithm for finding the optimal constrained unsatisfiable subsets; (2) a method for re-using relevant information over multiple algorithm calls; and (3) methods exploiting domain-specific information to speed up the explanation sequence generation. We experimentally validated our algorithms on a large number of CSP problems. We found that our algorithms outperform the MUS approach in terms of explanation quality and computational time (on average up to 56 % faster than a standard MUS approach).