High Performance SAT-based Constraint Programming System using Hybrid Encoding
| 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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2016: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究成果の意義は，SAT符号化の新しい方向性を開拓した点，既存のCPシステムでは求解困難な問題に対して，より高性能な推論基盤の候補を提供した点である．また重要な応用の1つとして，システム生物学やグラフ上の問題にも適用可能な多目的最適化問題への応用を示したことも挙げられる．CPシステムは様々な分野に応用される実用性が高いシステムであり，研究成果の産業分野への応用も期待できると考えられる．
|
Report
(4 results)
Research Products
(41 results)
