2020 Fiscal Year Research-status Report

Acceleration of SAT-based CSP Solvers using MDD

Research Project

Project/Area Number	20K11748
Research Institution	Kobe University
Principal Investigator	宋剛秀神戸大学, 情報基盤センター, 准教授 (00625121)
Project Period (FY)	2020-04-01 – 2023-03-31
Keywords	SATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング
Outline of Annual Research Achievements	近年，SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない，制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している．本研究の目的は，SAT型CSPソルバーの高速化であり, そのために MDD (Multi-valued Decision Diagram) を用いたCSPの正規化と，MDD が表す制約 (MDD制約) のSAT符号化を研究開発する．本研究の意義は, SAT型CSPソルバーの新しい一方式を開拓できる点，既存のCSPソルバーでは求解困難な問題に対して，より高性能な推論基盤を提供できる点である．CSPソルバーはスケジューリング問題, パッキング問題, 時間割問題,クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く，研究成果の産業分野への応用も期待できる． 2020年度は研究計画に記載された「(A) MDD 制約を用いた内包的制約，外延的制約, グローバル制約の正規化の研究」の研究環境を整えて研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った． (A) については，正規化方法を実装するSAT型CSPソルバー sCOP の研究開発を進めた． (C) については，一層平面配置配線問題への応用を研究し，国内の研究会で発表を行った．
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 当初の計画通り，2020年度は「(A) MDD 制約を用いた内包的制約，外延的制約, グローバル制約の正規化の研究」の研究を進めた．また当初の計画とは異なるが，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について先行して，調査研究を行った．これらより本研究課題は概ね順調に進展していると考えている．
Strategy for Future Research Activity	2021年度は計画通り「(A) MDD 制約を用いた内包的制約，外延的制約, グローバル制約の正規化の研究」および「(B) MDD 制約のSAT符号化の研究」の研究を進める予定である．また「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」についても可能であれば調査を進める．
Causes of Carryover	未使用額は100円に満たず，計画どおりに予算を使用した．次年度も計画通り予算を使用する予定である．