Planning under uncertainty via stochastic satisfiability
Stephen M. Majercik · National Conference on Artificial Intelligence · 1999
I describe a new planning technique that efficiently solves probabilistic propositional planning problems by converting them into instances of stochastic satisfiability (SSAT) and solving these problems instead. This is the first work extending the planning-as-satisfiability paradigm to stochastic domains. I make fundamental contributions in two areas: the solution of SS AT problems and the solution of probabilistic planning problems. I first describe three SSAT solvers: two exact solvers, based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, and one approximation technique. The first exact solver finds the optimal solution (a setting of variables in the SSAT problem that maximizes the probability of a satisfying assignment). The second applies bounding arguments to efficiently identify the first solution whose probability of satisfaction exceeds a prespecified threshold. I explore the application of several well-known DPLL heuristics to the solution of SSAT problems and empirically demonstrate that, while they improve performance significantly in randomly generated SS AT problems, in SSAT encodings of planning problems a simple heuristic based on temporal order dominates. The approximate solver uses a randomized approximation scheme (with or without hillclimbing) to rapidly identify a good solution to the SSAT problem. The epsilon-delta bound on the time required to evaluate SSAT solutions is polynomial in the size of the SSAT encoding v. exponential for the exact methods. In the second half of the dissertation, I describe two probabilistic planners: MAXPLAN (for unobservable domains) and ZANDER (for partially observable domains). MAXPLAN converts a dynamic-belief-net representation of a noncontingent planning problem into an instance of E-MAJSAT, a restricted type of SSAT problem in which existentially quantified variables precede randomly quantified variables. ZANDER solves general contingent planning problems by using a more general type of SSAT encoding in which existentially quantified and randomly quantified variables are interleaved. The conversion and solution algorithms exploit the structure of the domain, including factoring in the state representation and asymmetry in the distributions of propositions resulting from the application of actions. ZANDER can solve arbitrary, goal-oriented, finite-horizon partially observable Markov decision processes (POMDPS). An empirical study comparing ZANDER'S performance to that of three other leading probabilistic planners—a dynamic programming POMDP algorithm, MAHINUR, and SENSORY GRAPHPLAN (SGP)—shows that ZANDER'S performance equals or betters that of these planners on a range of problems. ZANDER finds optimal contingent plans as much as two orders of magnitude faster, in spite of the fact that MAHINUR and SGP are specialized to more restricted classes of problems. In addition, experiments indicate that further significant efficiency gains will be possible, thus allowing ZANDER to scale up to larger problems.