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

TL;DR

This paper introduces a symbolic SAT-based algorithm for almost-sure reachability in POMDPs, focusing on small strategies, and demonstrates its scalability through experimental results.

Contribution

It presents a novel SAT-encoding approach for finding small-memory strategies in POMDPs, improving scalability over explicit methods.

Findings

The SAT-based algorithm efficiently handles large POMDPs.

Small-memory strategies are sufficient in many practical cases.

Experimental results show improved scalability of the approach.

Abstract

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.