Sciweavers

AIPS
2006

Lemma Reusing for SAT based Planning and Scheduling

13 years 5 months ago
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.
Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, K
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2006
Where AIPS
Authors Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, Koji Iwanuma
Comments (0)