On the utility of landmarks in SAT based planning

摘要

Landmarks have been successfully employed in sequential planning, especially in the design of heuristic functions. However, little attention has been paid on exploiting landmarks in parallel planning. Here we propose a way to use the information of landmarks in SAT based planning, which is a successful framework for generating parallel plans. Specifically, we propose a way to encode landmarks and their orderings of a planning task into clauses, which are then integrated into the encoding of the task. We call those clauses landmark clauses. Landmark clauses are additional constraints that have the potential to help a SAT solver prune its search space considerably. However, for modern SAT solvers that employ more advanced reasoning or clause learning techniques, the effect of landmark clauses could be not intuitive. Therefore, our major work is giving examples and further identifying conditions under which landmark clauses are not logically redundant. We identify types of landmark clauses that cannot be derived by unit propagation, binary resolution or hyper resolution. Importantly, we prove that not all landmark clauses are redundant in terms of the UP-redundancy that was proposed by Sideris and Dimopoulos in 2010. We also conducted experiments on benchmarks from International Planning Competitions. The results show that MiniSat, a state-of-the-art SAT solver with the clause learning ability, with landmark clauses can be more efficient than it without landmark clauses on some hard planning problems. Therefore, we argue that landmarks and their orderings have promising effects in speeding up SAT based planning methods.