[1E2-OS-3a] AI における離散構造処理と制約充足(1)

[1E2-OS-3a-03] A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition

〇宋 剛秀¹、Le Berre Daniel^3,4、番原 睦則²、田村 直之¹ (1. 神戸大学、2. 名古屋大学、3. CRIL-CNRS, UMR 8188、4. Université d'Artois)

キーワード：命題論理における充足可能性判定問題、制約充足問題、SAT ソルバー、CSP ソルバー

制約充足問題 (CSP) は, 与えられた制約を全て充足する値割当てを求める問
題である. CSP には, 人工知能およびオペレーションズ・リサーチにおける幅
広い応用がある. XCSP3 は, CSP を記述できる主要な制約言語の1つであり，
105種類2万3千問を超える問題例が XCSP3 のデータベースから利用可能である．
また2018年には, XCSP3ソルバーの国際競技会が開催されており, 18 のソルバー
が参加した.

本論文では, 現在開発中の CSP ソルバー sCOP とその2018年XCSP3競技会の結
果について述べる. sCOP はSAT型ソルバーであり, CSP をSAT問題へと符号化
し, SATソルバーを用いて解を求める. 現在, sCOP では順序符号化と対数符号
化を利用することができ, 最新の SAT ソルバーをバックエンドに利用可能で
ある. 2018年XCSP3競技会において, sCOP はCSP・スタンダード・逐次部門と
CSP・スタンダード・並列部門の2部門に参加登録し, その両部門で優勝した．