Investigating the effect of relevance and reachability constraints on SAT encodings of planning

Recently, satisfiability (SAT) techniques have been shown to be more efficient at extracting solutions from a planning graph in Graphplan (Blum & Furst 1995) than the standard backward search(Kautz & Selman 1998). Graphplan gains efficiency from forward propagation and backward use of mutual exclusion constraints. The utility of SAT techniques for solution extraction raises two important questions: (a) Are the mutual exclusion constraints equally useful for so-lution extraction with SAT encodings? (b) If so, are there additional types of propagated constraints that can benefit them even more? Our ongoing research investigates these two questions. The mutual exclusion relations (mutex) used in the stan-dard Graphplan, that we shall refer to as fmutex constraints, are propagated by the following rules: Two facts P and Q are fmutex if all actions supporting P are pair-wise fmu-tex with all actions supporting Q. Two actions are fmu-tex if action A 1 deletes another action