Amol D. Mali
A classical planning problem is the problem of computing a sequence of actions that transforms one state of the world into the desired. Traditional planners cast planning as a "split and prune" type search. These are called "refinement planners" since they start with a null plan and refine it by adding constraints. It has been shown recently that planning problems are far 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 and preprocessing that traditional planners use. 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, to make a more exible and efficient exploration of the encodings possible.