A Study on Extending SAT Solvers with Cardinality Constraints and its Applications

2015 Fiscal Year Final Research Report

• 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
• Keywords: SATソルバー / 基数制約 / SAT符号化 / 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.

Free Research Field

知能情報処理