Lemma Reusing for SAT based Planning and Scheduling

In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches generate a sequence of SAT problems which become larger and larger. A SAT solver needs to solve the problems until it encounters a satisfiable SAT problem. Many state-of-the-art SAT solvers learn lemmas called conflict clauses to prune redundant search space, but lemmas deduced from a certain SAT problem can not apply to solve other SAT problems. However, in certain SAT encodings of planning and scheduling, we prove that lemmas generated from a SAT problem are reusable for solving larger SAT problems. We implemented the lemma-reusing planner (LRP) and the lemma-reusing job shop scheduling problem solver (LRS). The experimental results show that LRP and LRS are faster than lemma-no-reusing ones. Our approach makes it possible to use the latest SAT solvers more efficiently for the SAT based planning and scheduling.

• Type: Conference
• Year: 2006
• Where: AIPS
• Authors: Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, Koji Iwanuma
• Keywords: AIPS 2006, Artificial Intelligence, SAT Based Planning, SAT Problems, SAT Solvers