SAT型制約ソルバーを用いたナンバーリンクの解法
Bibliographic Information
- Other Title
-
- Solving Numberlink by a SAT-based Constraint Solver
Abstract
制約充足問題 (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.
Journal
-
- DAシンポジウム2014論文集
-
DAシンポジウム2014論文集 2014 215-220, 2014-08-21
- Tweet
Keywords
Details
-
- CRID
- 1050855522055699584
-
- NII Article ID
- 170000084795
-
- Web Site
- http://id.nii.ac.jp/1001/00102757/
-
- Text Lang
- ja
-
- Article Type
- conference paper
-
- Data Source
-
- IRDB
- CiNii Articles