Faster probabilistic planning through more efficient stochastic satisfiability problem encodings

The propositional contingent planner ZANDER solves finite-horizon, partially observable, probabilistic planning prob-lems at state-of-the-art-speeds by converting the planning problem to a stochastic satisfiability (SSAT) problem and solving that problem instead (Majercik 2000). ZANDER ob-tains these results using a relatively inefficient SSAT encod-ing of the problem (a linear action encoding with classical frame axioms). We describe and analyze three alternative SSAT encodings for probabilistic planning problems: a lin-ear action encoding with simple explanatory frame axioms, a linear action encoding with complex explanatory frame ax-ioms, and a parallel action encoding. Results on a suite of test problems indicate that linear action encodings with sim-ple explanatory frame axioms and parallel action encodings show particular promise, improving ZANDER’s efficiency by as much as three orders of magnitude