On the Hybrid Propositional Encodings of Planning

Recently, casting planning as propositional satisfiability (SAT) has been shown to be an efficient technique of plan synthesis. This article is a response to the recently proposed challenge of developing novel propositional encodings that are based on a combination of different types of plan refinements and characterizing the tradeoffs. We refer to these encodings as hybrid encodings. An investigation of these encodings is important, because this can give insights into what kinds of planning problems can be solved faster with hybrid encodings. Encodings based on partial–order planning and state–space planning have been reported in previous research. We propose a new type of encoding called a unifying encoding that subsumes these two encodings. We also report on several other hybrid encodings. Next, we show how the satisfiability framework can be extended to incremental planning. State–space encoding is attractive because of its lower size and causal encoding is attractive because of its highest flexibility in reordering steps. We show that hybrid encodings have a higher size and a lower flexibility in step reordering and, thus, do not combine the best of these encodings. We discuss in detail several specific planning scenarios where hybrid encodings are likely to be superior to nonhybrid encodings.