1999 Fiscal Year Final Research Report Summary
Solving Real-World Combinatorial Problems using High-Speed SAT-Algorithms
| Project/Area Number |
09480055
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
IWAMA Kazuo Kyoto Univ., Graduate School of Informatics, Professor, 情報学研究科, 教授 (50131272)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGINO Hiroyuki Kyoto Univ., Graduate School of Informatics, Instructor, 情報学研究科, 助手 (40144323)
YASUOKA Koichi Kyoto Univ., Data Processing Center, Associate Professor, 大型計算機センター, 助教授 (20230211)
OKABE Yasuo Kyoto Univ., Graduate School of Informatics, Associate Professor, 情報学研究科, 助教授 (20204018)
IWAMOTO Chuzo Hiroshima Univ., Dept. of Industrial and Systems Enginee Associate Professor, 工学部, 助教授 (60274495)
MIYAZAKI Shuichi Kyoto Univ., Graduate School of Informatics, Instructor, 情報学研究科, 助手 (00303884)
|
|---|
| Project Period (FY) |
1997 – 1999
|
| Keywords | real-world problems / CNF Satisfiability / Partial MAXSAT / student assignment / local search algorithms / parallelization / vectorization / PVM |
|---|
| Research Abstract |
The purpose of this research is to develop general method for solving intractable real-world problems. Our strategy is not to solve each problem directly but to translate it into CNF Satis-fiability(SAT), solve SAT, and translate the solution of SAT back to the solution of the original problem. We can expect several advantages: (1) It is easy to translate combinatorial problems into SAT. (2) We can exploit existing fast SAT algorithms.
In this research, we first formalized real-world problems and established translation method from real-world problems into SAT so that automatic translations are possible.
Next, to examine the efficiency of our approach, we conducted experiments. We adopted the time-scheduling problem and the student assignment problem, which are popular problems in universities. Our experimental results show that for both problems our method performed better than existing direct algorithms.
Finally, we attempted speedup of local search algorithms for SAT via parallelization. We used vector computer VPP 800and PVM for this purpose. The nature of local search algorithms fits for parallelization because we can run several search paths independently. Furthermore, we need little communication. By experiments, we showed that we can obtain ideal speedup as expected. We tried several benchmark instances and were able to solve some instances which had not been solved by any algorithms.
|
