DSatz: A Directional SAT Solver for Planning

(Appears as a regular paper in the proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI), IEEE Computer Society, Washington D.C, Nov. 2002, pp. 199-208.) 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 S...

• Type: Conference
• Year: 2002
• Where: ICTAI
• Authors: Mark Iwen, Amol Dattatraya Mali
• Keywords: Artificial Intelligence, Backward Search, ICTAI 2002, Sat Encoding, SAT-based Planners