Compact Policies for Fully-Observable Non-Deterministic Planning as SAT

TL;DR

This paper introduces a compact SAT-based encoding for FOND planning that efficiently produces strong cyclic policies, with variations for different planning assumptions, and compares its performance against existing methods.

Contribution

The paper presents a novel, compact SAT encoding for FOND planning capable of generating strong cyclic policies, including variants for different planning scenarios.

Findings

The SAT encoding produces competitive and often superior policies compared to existing planners.

Empirical evaluation demonstrates the efficiency and effectiveness of the proposed approach.

Analysis of probabilistic problems highlights the strengths and limitations of current FOND planners.

Abstract

Fully observable non-deterministic (FOND) planning is becoming increasingly important as an approach for computing proper policies in probabilistic planning, extended temporal plans in LTL planning, and general plans in generalized planning. In this work, we introduce a SAT encoding for FOND planning that is compact and can produce compact strong cyclic policies. Simple variations of the encodings are also introduced for strong planning and for what we call, dual FOND planning, where some non-deterministic actions are assumed to be fair (e.g., probabilistic) and others unfair (e.g., adversarial). The resulting FOND planners are compared empirically with existing planners over existing and new benchmarks. The notion of "probabilistic interesting problems" is also revisited to yield a more comprehensive picture of the strengths and limitations of current FOND planners and the proposed SAT approach.