A Study on Extending SAT Solvers with Cardinality Constraints and its Applications
| Project/Area Number |
25330085
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
Koshimura Miyuki 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HASEGAWA Ryuzo 九州大学, 大学院システム情報科学研究院, 教授 (20274483)
FUJITA Hiroshi 九州大学, 大学院システム情報科学研究院, 准教授 (70284552)
Chikara Noriaki 徳山工業高等学校, 情報電子工学科, 助手 (50290804)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2015: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | SATソルバー / 基数制約 / SAT符号化 / MaxSAT応用 / MaxSATソルバー / 組合せ最適 |
|---|
| Outline of Final Research Achievements |
The major results of this study are as follows:
(1) Introduce a method of alternating different strategies into SAT solver in order to enhance its performance. (2) Devise two new SAT encodings Modulo Totalizer and Weighted Totalizer for cardinality constraints and give their space complexity. (3) Present methods for solving the following problems with MaxSAT; (i) inductive logic programming, (ii) coalition structure generation, and (iii) reconstructing AES key schedule images. (4) Introduce a mechanism to utilize unsat core in a MaxSAT solver QMaxSAT.
|
Report
(4 results)
Research Products
(27 results)
