High Performance SAT-based Constraint Programming System using Hybrid Encoding

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K16036
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Kobe University
• Principal Investigator: Soh Takehide 神戸大学, 情報基盤センター, 助教 (00625121)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: SATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング

Outline of Final Research Achievements

Constraint Satisfaction Problem (CSP) is a problem of finding an assignment that satisfies all the given constraints. CSP has various applications in both academia and industry and it is recognized as an important problem in the research area of Artificial Intelligence. In this research, we study a hybrid encoding method to realize a high performance CSP solving system using SAT solvers (SAT-based CP System). As a result, we succeeded in winning an international competition and solving problems that cannot be solved by existing systems.

Free Research Field

制約プログラミング

Academic Significance and Societal Importance of the Research Achievements

本研究成果の意義は，SAT符号化の新しい方向性を開拓した点，既存のCPシステムでは求解困難な問題に対して，より高性能な推論基盤の候補を提供した点である．また重要な応用の1つとして，システム生物学やグラフ上の問題にも適用可能な多目的最適化問題への応用を示したことも挙げられる．CPシステムは様々な分野に応用される実用性が高いシステムであり，研究成果の産業分野への応用も期待できると考えられる．