Name
Abstract | ||
|---|---|---|
In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches gen- erate 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 con- flict clauses to prune redundant search space, but lem- mas deduced from a certain SAT problem can not ap- ply to solve other SAT problems. However, in certain SAT encodings of planning and scheduling, we prove that lemmas generated from a SAT problem arereusable for solving larger SAT problems. We implemented the lemma-reusing planner (LRP) and the lemma-reusing job shop scheduling problem solver (LRS). The exper- imental results show that LRP and LRS are faster than lemma-no-reusing ones. Our approach makes it possi- ble to use the latest SAT solvers more efficiently for the SAT based planning and scheduling. |
Year | Venue | Keywords |
|---|---|---|
2006 | ICAPS | satisfiability,sat solver,search space |
Field | DocType | Citations |
#SAT,Mathematical optimization,Computer science,Reuse,Job shop scheduling problem,Scheduling (computing),Boolean satisfiability problem,Sat problem,Theoretical computer science,Solver,Lemma (mathematics) | Conference | 8 |
PageRank | References | Authors |
0.61 | 19 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hidetomo Nabeshima | 1 | 154 | 14.88 |
| Takehide Soh | 2 | 79 | 7.97 |
| Katsumi Inoue | 3 | 1271 | 112.78 |
| Koji Iwanuma | 4 | 138 | 17.65 |