Presentation	2003/5/22 Effective SAT Planning by Lemma-Reusing Hidetomo NABESHIMA, Hirohito NOZAWA, 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 for improving efficiency of SAT planning by lemma-reusing. Generally, a lemma derived from a SAT problem can not apply to other SAT problems. However, we prove that lemmas generated by Chaff which is the fastest SAT solver in the world are applicable to other SAT problems generated in SAT planning. We propose a new SAT planning approach LRP which reuses such lemmas, and prove the correctness. The experimental results show that LRP is 160% faster than Blackbox that does not reuse lemmas.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	SAT planning / Satisfiablitiy / Lemma
Paper #	AI2003-9
Date of Issue

Conference Information
Committee	AI
Conference Date	2003/5/22(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	JPN
Title (in Japanese)	(See Japanese page)
Sub Title (in Japanese)	(See Japanese page)
Title (in English)	Effective SAT Planning by Lemma-Reusing
Sub Title (in English)
Keyword(1)	SAT planning
Keyword(2)	Satisfiablitiy
Keyword(3)	Lemma
1st Author's Name	Hidetomo NABESHIMA
1st Author's Affiliation	Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi()
2nd Author's Name	Hirohito NOZAWA
2nd Author's Affiliation	AM Corporation,
3rd Author's Name	Koji IWANUMA
3rd Author's Affiliation	Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi
Date	2003/5/22
Paper #	AI2003-9
Volume (vol)	vol.103
Number (no)	103
Page	pp.pp.-
#Pages	6
Date of Issue