2026-03-08T14:38:25Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00102780 2025-01-21T10:42:01Z 6164:6165:7651:7653

SAT型制約ソルバーを用いたナンバーリンクの解法 Solving Numberlink by a SAT-based Constraint Solver 田村, 直之 宋, 剛秀 番原, 睦則 鍋島, 英知 Naoyuki, Tamura Takehide, Soh Mutsunori, Banbara Hidetomo, Nabeshima アルゴリズム・ソルバ 制約充足問題 (CSP) は与えられた制約を満たす解を探索する問題であり，多くの組合せ問題は CSP として定式化できる．SAT 型制約ソルバーは，CSP を命題論理の充足可能性判定問題 (SAT) に符号化し，SAT ソルバーを用いて探索することにより，CSP の解を求めるプログラムである．ここでは，国際的な競技会で優秀な成績を収めている制約ソルバー Sugar および SAT ソルバー GlueMiniSat を用い，SAT 型制約ソルバーでナンバーリンク問題の高速な求解が可能であることを示す．また，制約記述には Scala 上の制約プログラミングシステムであるCopris を用いる．これにより，提案するシステムは高い拡張性も実現している． 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. conference paper 情報処理学会 2014-08-21 application/pdf DAシンポジウム2014論文集 2014 215 220 https://ipsj.ixsq.nii.ac.jp/record/102780/files/IPSJ-DAS2014040.pdf jpn