Contingent Planning Under Uncertainty via Stochastic Satisfiability Stephen M. Majercik and Michael L. Littman Abstract: We describe two new probabilistic planning techniques---C-MAXPLAN and ZANDER---that generate contingent plans in probabilistic propositional domains. Both operate by transforming the planning problem into a stochastic satisfiability problem and solving that problem instead. C-MAXPLAN encodes the problem as an E-MAJSAT instance, while ZANDER encodes the problem as an SSAT instance. Although SSAT problems are in a higher complexity class than E-MAJSAT problems, the problem encodings produced by ZANDER are substantially more compact and appear to be easier to solve than the corresponding E-MAJSAT encodings. Preliminary results for ZANDER indicate that it is competitive with existing planners on a variety of problems.