Investigating the Effect of Relevance and Reachability Constraints on SAT Encodings of Planning

Minh Binh Do, Biplav Srivastava, and Subbarao Kambhampati

Currently, Graphplan and Blackbox, which converts Graph-plan’s plan graph into the satisfaction (SAT) problem, are two of the most successful planners. Since Graphplan gains its efficiency from the forward propagation of reachability based mutual exclusion constraints (mutex) and their backward use, it has been believed that SAT encoding will also benefit from mutexes. In this paper, we will try to answer two important questions: (1) Are mutual exclusions actually useful for solution extraction in SAT encoding? (2) Are there other useful constraints that can be propagated on the planning graph which may help SAT solvers ? Our experiments with systematic solvers Relsat and Satz shows that though forward mutexes are useful in general, there are domains in which mutex constraints can slow down search. Moreover, we introduce the notion of backward mutex and their propagation which is based on relevance analysis and implement it in Blackbox. We find that the addition of relevance based backward mutual exclusions helps speedup the Relsat solver in solving the SAT encoding of many standard planning problems.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.