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

Currently, Graphplan and Blackbox, which converts Graphplan'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...

• Type: Conference
• Year: 2000
• Where: AIPS
• Authors: Minh Binh Do, Biplav Srivastava, Subbarao Kambhampati
• Keywords: AIPS 2000, Artificial Intelligence, Mutex Constraints, Mutual Exclusion Constraints, Mutual Exclusions