2009 Fiscal Year Final Research Report
A Study of Advanced and Effective SAT Planning and Scheduling
| Project/Area Number |
19700135
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
NABESHIMA Hidetomo University of Yamanashi, 大学院・医学工学総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Keywords | 充足可能性問題 / プランニング / スケジューリング / 分散協調 |
|---|
| Research Abstract |
Propositional satisfiability (SAT) problems and its high performance solvers are used for solving various problems, such as planning and scheduling, which are encoded into SAT instances. Generally, SAT encoding approaches need to solve multiple SAT instances. In order to solve such multiple SAT instances, we have developed a distributed and cooperative SAT solver SatCube, which reuse lemmas, hypotheses and models during the search process and can solve multiple SAT instances efficiently. We have studied SAT planning to extend the application area based on ordered encoding, and proposed various speed-up techniques for SAT scheduling.
|
