A Compact and Efficient SAT Encoding for Planning

In the planning-as-SAT paradigm there have been numerous recent developments towards improving the speed and scalability of planning at the cost of finding a step-optimal parallel plan. These developments have been towards: (1) Query strategies that efficiently yield approximately optimal plans, and (2) Having a SAT procedure compute plans from relaxed encodings of the corresponding decision problems in such a way that conflicts in a plan arising from the relaxation are resolved cheaply during a post-processing phase. In this paper we examine a third direction of tightening constraints in order to achieve a more compact, efficient, and scalable SAT-based encoding of the planning problem. For the first time, we use lifting (i.e., operator splitting) and factoring to encode the corresponding n-step decision problems with a parallel action semantics. To ensure compactness we exploit reachability and neededness analysis of the plangraph. Our encoding also captures state-dependent mutex co...

• Type: Conference
• Year: 2008
• Where: AIPS
• Authors: Nathan Robinson, Charles Gretton, Duc Nghia Pham, Abdul Sattar
• Keywords: AIPS 2008, Artificial Intelligence, Optimal Sat-based Planners, SAT-based Planners, Scalable Sat-based Encoding