Refinement-Based Planning as Satisfiability

Abstract

It has been shown recently that planning problems are easier to solve when they are cast as model finding problems. Some schemes for automated generation of the encodings of the planning problems in propositional logic have been designed. However these schemes lack several of the refinements that traditional split & prune type planners do. We show that it is possible to transfer these refinements into the encodings. Since no single encoding has been shown to have the smallest size and the best performance, it is necessary to know what the space of the encodings is. Knowing this space makes a more flexible and efficient design of encodings possible. We show how refinements can be used to generate one such space of encodings. We examine this space and provide the asymptotic sizes of the encodings. This inclusion of refinements into the encodings results in more flexible encodings, some of which are smaller. Our work bridges the gap between the previous research in planning (planning as s...