# Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 39 references that are in the map.
- First posted on arXiv 11 Nov 2025.

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

- [Robust Finite-State Controllers for Uncertain POMDPs](https://mlsanity.com/paper/2009.11459/) (2020)
- [Distributionally Robust Partially Observable Markov Decision Process with Moment-based Ambiguity](https://mlsanity.com/paper/1906.05988/) (2019)
- [dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts](https://mlsanity.com/paper/2101.07202/) (2021)
- [A Practitioner's Guide to MDP Model Checking Algorithms](https://mlsanity.com/paper/2301.10197/) (2023)
- [Optimistic Value Iteration](https://mlsanity.com/paper/1910.01100/) (2019)
- [Robust Almost-Sure Reachability in Multi-Environment MDPs](https://mlsanity.com/paper/2301.11296/) (2023)
- [Witty: An Efficient Solver for Computing Minimum-Size Decision Trees](https://mlsanity.com/paper/2412.11954/) (2024)
- [Policies Grow on Trees: Model Checking Families of MDPs](https://mlsanity.com/paper/2407.12552/) (2024)
- [Small Decision Trees for MDPs with Deductive Synthesis](https://mlsanity.com/paper/2501.10126/) (2025)
- [Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives](https://mlsanity.com/paper/2406.02871/) (2024)

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

- [Scaling Observation-aware Planning in Uncertain Domains](https://mlsanity.com/paper/2605.22364/) (2026)
- [Bellman-Certified Rounding for Sparse Policy Deployment in MDPs](https://mlsanity.com/paper/2610.00325/) (2026)

## Abstract (arXiv)

The ability to compute reward-optimal policies for given and known finite Markov decision processes (MDPs) underpins a variety of applications across planning, controller synthesis, and verification. However, we often want policies (1) to be robust, i.e., they perform well on perturbations of the MDP and (2) to satisfy additional structural constraints regarding, e.g., their representation or implementation cost. Computing such robust and constrained policies is indeed computationally more challenging. This paper contributes the first approach to effectively compute robust policies subject to arbitrary structural constraints using a flexible and efficient framework. We achieve flexibility by allowing to express our constraints in a first-order theory over a set of MDPs, while the root for our efficiency lies in the tight integration of satisfiability solvers to handle the combinatorial nature of the problem and probabilistic model checking algorithms to handle the analysis of MDPs. Experiments on a few hundred benchmarks demonstrate the feasibility for constrained and robust policy synthesis and the competitiveness with state-of-the-art methods for various fragments of the problem.