- 受賞者
- 情報基盤センター 宋剛秀 助教
- 受賞日
- 2018年8月28日
- 受賞名
- 2018年XCSP3競技会
スタンダードソルバー?逐次?CSP部門 1位
スタンダードソルバー?並列?CSP部門 1位 - 業績名
- sCOP: SAT-based Constraint Programming System
概要
制約充足問題 (CSP) は、与えられた制約条件を満たす解を求める問題です。
CSPは様々な産業分野に応用されているだけでなく、解を求めることが非常に困難な問題としてソフトウェアや人工知能などの研究分野における重要な研究課題となっています。CSPは欧米を中心として活発に研究が進められています。
XCSP3 競技会は、そのような CSP を解くプログラム (CSP ソルバー) の性能を競う国際競技会の一つで、2005年にその前身が始まった歴史のある競技会です。
今回 XCSP3 競技会の2部門へ出場し両方で1位という良い成績を収めた CSPソルバー sCOP の一番の特徴は、与えられた CSPをSATと呼ばれるより簡単な表現をもつ問題へと”符号化”して、SATを解くプログラムであるSATソルバーを用いてCSPを解くことです (図1)。さらに、効率の良い順序符号化と呼ばれる符号化方法を用いることで、高性能なCSPソルバーを実現しています。
今後の展望
CSPを拡張した問題として、与えられた制約を満たす解の中で最適なもの（最適解）を探索する問題である制約最適化問題 (COP) があります。病院での勤務シフトの作成やスポーツの対戦スケジュール作成など、COP は身近な応用がたくさんある重要な問題です。今後の課題としてsCOPをCOPに対応できるように拡張することが挙げられます。
