| 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)
|
|---|
| 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.
|
