Compact Policies for Fully-Observable Non-Deterministic Planning as SAT
  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.
