Presentation 2006-05-18
Effective SAT Planning and SAT Scheduling by Lemma Reusing
Hidetomo NABESHIMA, Takehide SOH, Katsumi INOUE, Koji IWANUMA,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) 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.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) SAT / planning / scheduling
Paper # AI2006-4
Date of Issue

Conference Information
Committee AI
Conference Date 2006/5/11(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Artificial Intelligence and Knowledge-Based Processing (AI)
Language ENG
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
1st Author's Name Hidetomo NABESHIMA
1st Author's Affiliation Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi()
2nd Author's Name Takehide SOH
2nd Author's Affiliation Graduate School of Science and Technology, Kobe University
3rd Author's Name Katsumi INOUE
3rd Author's Affiliation National Institute of Informatics
4th Author's Name Koji IWANUMA
4th Author's Affiliation Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi
Date 2006-05-18
Paper # AI2006-4
Volume (vol) vol.106
Number (no) 38
Page pp.pp.-
#Pages 6
Date of Issue