Sciweavers

Share
AIPS
2008

A Compact and Efficient SAT Encoding for Planning

10 years 20 days ago
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...
Nathan Robinson, Charles Gretton, Duc Nghia Pham,
Added 02 Oct 2010
Updated 02 Oct 2010
Type Conference
Year 2008
Where AIPS
Authors Nathan Robinson, Charles Gretton, Duc Nghia Pham, Abdul Sattar
Comments (0)
books