# A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Nov 2015.

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

- [Safe Reinforcement Learning via Shielding under Partial Observability](https://mlsanity.com/paper/2204.00755/) (2022)
- [Flexible FOND Planning with Explicit Fairness Assumptions](https://mlsanity.com/paper/2103.08391/) (2021)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination](https://mlsanity.com/paper/2105.12908/) (2021)
- [Natural Strategic Ability in Stochastic Multi-Agent Systems](https://mlsanity.com/paper/2401.12170/) (2024)
- [Explainable Representation of Finite-Memory Policies for POMDPs using Decision Trees](https://mlsanity.com/paper/2411.13365/) (2024)

## Abstract (arXiv)

POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach.