SAT型制約ソルバーを用いたナンバーリンクの解法

• Item type: Symposium(1)
• 公開日: 2014-08-21
• タイトル: SAT型制約ソルバーを用いたナンバーリンクの解法
• タイトル / 言語: en
• タイトル: Solving Numberlink by a SAT-based Constraint Solver
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: アルゴリズム・ソルバ
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 山梨大学医学工学総合研究部
• 著者所属(英): en
• 著者所属(英): Kobe University
• 著者所属(英): en
• 著者所属(英): Kobe University
• 著者所属(英): en
• 著者所属(英): Kobe University
• 著者所属(英): en
• 著者所属(英): Yamanashi University
• 著者名: 田村, 直之; 宋, 剛秀; 番原, 睦則; 鍋島, 英知
• 著者名(英): Naoyuki, Tamura; Takehide, Soh; Mutsunori, Banbara; Hidetomo, Nabeshima
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 制約充足問題 (CSP) は与えられた制約を満たす解を探索する問題であり，多くの組合せ問題は CSP として定式化できる．SAT 型制約ソルバーは，CSP を命題論理の充足可能性判定問題 (SAT) に符号化し，SAT ソルバーを用いて探索することにより，CSP の解を求めるプログラムである．ここでは，国際的な競技会で優秀な成績を収めている制約ソルバー Sugar および SAT ソルバー GlueMiniSat を用い，SAT 型制約ソルバーでナンバーリンク問題の高速な求解が可能であることを示す．また，制約記述には Scala 上の制約プログラミングシステムであるCopris を用いる．これにより，提案するシステムは高い拡張性も実現している．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Constraint Satisfaction Problem (CSP) is a problem to find a solution satisfying all given constraints, and many combinatorial problems can be formalized as a CSP. SAT-based constraint solver is a program to find a solution of a given CSP by encoding it to a Boolean satisfiability testing program (SAT) and searching a solution with a SAT solver. In this paper, we show a SAT-based constraint solver can efficiently solve Numberlink puzzles with Sugar and GlueMiniSat solvers which performed well at the international solver competitions. A constraint programming system Copris on a Scala programming language is used for a constraint modeling. Therefore, the proposed Numberlink solver also realizes high extensibility.
• 書誌情報: DAシンポジウム2014論文集; 巻 2014, p. 215-220, 発行日 2014-08-21
• 出版者 / 言語: ja
• 出版者: 情報処理学会