loading...
DSatz: A Directional SAT Solver for Planning
Washington, DC November 04-November 06
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TAI.2002.118080514th IEEE International Conference on ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Mark Iwen, University of Wisconsin at Milwaukee
Amol Dattatraya Mali, University of Wisconsin at Milwaukee
SAT-based planners have been characterized as disjunctive planners that maintain a compact representation of search space of action sequences. Several ideas from refinement planners (conjunctive planners) have been used to improve performance of SAT-based planners or get a better understanding of planning as SAT. One important lesson from refinement planning is that backward search being goal directed can be more efficient than forward search. Another lesson is that bidirectional search is generally not efficient. This is because the forward and backward searches can miss each other. Though effect of direction of plan refinement (forward, backward, bidirectional etc.) on efficiency of plan synthesis has been deeply investigated in refinement planning, the effect of directional solving of SAT encodings is not investigated in depth. We solved several propositional encodings of benchmark planning problems with a modified form (DSatz) of the systematic SAT solver Satz. DSatz offers 21 options for solving a SAT encoding of a planning problem, where the options are about assigning truth values to action and/or fluent variables in forward or backward or both directions, in an intermittent or non-intermittent style. Our investigation shows that backward search on plan encodings (assigning values to fluent variables first, starting with goal) is very inferior. We also show bidirectional solving options and forward solving options turn out to be far more efficient than other solving options. Our empirical results show that the efficient systematic solver Satz which exploits variable dependencies can be significantly enhanced with use of our variable ordering heuristics which are also computationally very cheap to apply. Our main results are that directionality does matter in solving SAT encodings of planning problems and that certain directional solving options are superior to others.
Citation:
Mark Iwen, Amol Dattatraya Mali, "DSatz: A Directional SAT Solver for Planning," ictai, pp.199, 14th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.