Research and Development of a New Constraint Programming System based on SAT

2018 Fiscal Year Final Research Report

• Project/Area Number: 16H02803
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Kobe University
• Principal Investigator: Tamura Naoyuki 神戸大学, 情報基盤センター, 教授 (60207248)
• Co-Investigator(Kenkyū-buntansha): 番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774) ; 宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121) ; 井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321) ; 鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 制約プログラミング / 充足可能性判定問題 / 命題論理

Outline of Final Research Achievements

SAT-based systems utilizing SAT solving technologies have been succeeding in various fields requiring highly efficient inference. In order to extend the SAT technology beyond its current application area, we conducted the research and development of SAT-based constraint programming systems in the following topics: (A) Extention to temporal logic, (B) Extention to multi-objective optimization problems, (C) Parallel solvers, and (D) Research and Development of application systems. As a result, we obtained several good accomplishments, such as winning at the international constraint solver competition, and solving problems which have not been solved with previous methods.

Free Research Field

情報科学・ソフトウェア

Academic Significance and Societal Importance of the Research Achievements

高度な推論を必要とする人工知能システムなどの実現を目的として，その基本技術となるSAT型CPシステムの研究開発を行った．開発したシステムの1つであるsCOPは，2018年の国際制約ソルバー競技会の2部門で優勝している．また，ペトリネットのデッドロック検出，研究室配属問題，時間割問題，テストケース生成，配線問題などへの応用研究を行い，これまでよりも優れた結果を得た．