| Paper Abstract and Keywords |
| Presentation |
2006-05-18 11:10
Effective SAT Planning and SAT Scheduling by Lemma Reusing
Hidetomo Nabeshima (Univ. of Yamanashi), Takehide Soh (Kobe Univ.), Katsumi Inoue (NII), Koji Iwanuma (Univ. of Yamanashi) |
| Abstract |
(in Japanese) |
(See Japanese page) |
| (in English) |
In this paper, we propose a new approach, called {\itshape 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 {\itshape 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 {\itshape 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. |
| Keyword |
(in Japanese) |
(See Japanese page) |
| (in English) |
SAT / planning / scheduling / / / / / |
| Reference Info. |
IEICE Tech. Rep., vol. 106, no. 38, AI2006-4, pp. 19-24, May 2006. |
| Paper # |
AI2006-4 |
| Date of Issue |
2006-05-11 (AI) |
| ISSN |
Print edition: ISSN 0913-5685 |
| Download PDF |
|
| Conference Information |
| Committee |
AI |
| Conference Date |
2006-05-18 - 2006-05-18 |
| Place (in Japanese) |
(See Japanese page) |
| Place (in English) |
Kikai-Shinko-Kaikan Bldg. |
| Topics (in Japanese) |
(See Japanese page) |
| Topics (in English) |
|
| Paper Information |
| Registration To |
AI |
| Conference Code |
2006-05-AI |
| Language |
English (Japanese title is available) |
| Title (in Japanese) |
(See Japanese page) |
| Sub Title (in Japanese) |
(See Japanese page) |
| Title (in English) |
Effective SAT Planning and SAT Scheduling by Lemma Reusing |
| Sub Title (in English) |
|
| Keyword(1) |
SAT |
| Keyword(2) |
planning |
| Keyword(3) |
scheduling |
| Keyword(4) |
|
| Keyword(5) |
|
| Keyword(6) |
|
| Keyword(7) |
|
| Keyword(8) |
|
| 1st Author's Name |
Hidetomo Nabeshima |
| 1st Author's Affiliation |
University of Yamanashi (Univ. of Yamanashi) |
| 2nd Author's Name |
Takehide Soh |
| 2nd Author's Affiliation |
Kobe University (Kobe Univ.) |
| 3rd Author's Name |
Katsumi Inoue |
| 3rd Author's Affiliation |
National Institute of Infomatics (NII) |
| 4th Author's Name |
Koji Iwanuma |
| 4th Author's Affiliation |
University of Yamanashi (Univ. of Yamanashi) |
| 5th Author's Name |
|
| 5th Author's Affiliation |
() |
| 6th Author's Name |
|
| 6th Author's Affiliation |
() |
| 7th Author's Name |
|
| 7th Author's Affiliation |
() |
| 8th Author's Name |
|
| 8th Author's Affiliation |
() |
| 9th Author's Name |
|
| 9th Author's Affiliation |
() |
| 10th Author's Name |
|
| 10th Author's Affiliation |
() |
| 11th Author's Name |
|
| 11th Author's Affiliation |
() |
| 12th Author's Name |
|
| 12th Author's Affiliation |
() |
| 13th Author's Name |
|
| 13th Author's Affiliation |
() |
| 14th Author's Name |
|
| 14th Author's Affiliation |
() |
| 15th Author's Name |
|
| 15th Author's Affiliation |
() |
| 16th Author's Name |
|
| 16th Author's Affiliation |
() |
| 17th Author's Name |
|
| 17th Author's Affiliation |
() |
| 18th Author's Name |
|
| 18th Author's Affiliation |
() |
| 19th Author's Name |
|
| 19th Author's Affiliation |
() |
| 20th Author's Name |
|
| 20th Author's Affiliation |
() |
| 21st Author's Name |
|
| 21st Author's Affiliation |
() |
| 22nd Author's Name |
|
| 22nd Author's Affiliation |
() |
| 23rd Author's Name |
|
| 23rd Author's Affiliation |
() |
| 24th Author's Name |
|
| 24th Author's Affiliation |
() |
| 25th Author's Name |
|
| 25th Author's Affiliation |
() |
| 26th Author's Name |
/ / |
| 26th Author's Affiliation |
()
() |
| 27th Author's Name |
/ / |
| 27th Author's Affiliation |
()
() |
| 28th Author's Name |
/ / |
| 28th Author's Affiliation |
()
() |
| 29th Author's Name |
/ / |
| 29th Author's Affiliation |
()
() |
| 30th Author's Name |
/ / |
| 30th Author's Affiliation |
()
() |
| 31st Author's Name |
/ / |
| 31st Author's Affiliation |
()
() |
| 32nd Author's Name |
/ / |
| 32nd Author's Affiliation |
()
() |
| 33rd Author's Name |
/ / |
| 33rd Author's Affiliation |
()
() |
| 34th Author's Name |
/ / |
| 34th Author's Affiliation |
()
() |
| 35th Author's Name |
/ / |
| 35th Author's Affiliation |
()
() |
| 36th Author's Name |
/ / |
| 36th Author's Affiliation |
()
() |
| Speaker |
Author-1 |
| Date Time |
2006-05-18 11:10:00 |
| Presentation Time |
25 minutes |
| Registration for |
AI |
| Paper # |
AI2006-4 |
| Volume (vol) |
vol.106 |
| Number (no) |
no.38 |
| Page |
pp.19-24 |
| #Pages |
6 |
| Date of Issue |
2006-05-11 (AI) |