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
|
Project Status |
Completed (Fiscal Year 2009)
|
Budget Amount *help |
¥3,810,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥510,000)
Fiscal Year 2009: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2008: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2007: ¥1,600,000 (Direct Cost: ¥1,600,000)
|
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.
|
Report
(4 results)
Research Products
(23 results)