SMT ソルバを用いた Slitherlink パズルの解法

• 宮内, 哲夫

• 田中, 清史

Bibliographic Information

Other Title

• A Solution to the Slitherlink Puzzle Using SMT Solver

Abstract

Slitherlinkはペンシルパズルといわれるパズルに属し，その解の存在問題はNP-完全問題に属する[10]．これまでにいくつかの解法が提案されており，文献[1]では整数計画法を用いてこれまでの解法より高速に解けることを示している．また，文献[5]では制約ソルバーによる解法が示されている．本稿では，高速に解を得られる新たな定式化の方法を提案し，SMTソルバZ3を用いることで，サイズの大きい問題に対して既存の解法よりさらに高速に解けることを示す．

Slitherlink is one of pencil puzzles and an NP-complete problem[10]. Several solutions for it have been proposed. Literature [1] provides a solution by IP (integer programming) which is faster than the existing ones. Literature [5] shows a solution with using a constraint solver. This paper proposes a way of formulating the problem and shows it can obtain solutions for large-sized problems faster than the technique in [1], by utilizing the SMT solver, Z3.

Journal

• ゲームプログラミングワークショップ2017論文集

  ゲームプログラミングワークショップ2017論文集 2017 111-118, 2017-11-03

Keywords

• Slitherlink
• 解法
• SMT ソルバ
• Z3

Details

• CRID: 1050292572112753024
• NII Article ID: 170000176057
• Web Site: http://id.nii.ac.jp/1001/00183756/
• Text Lang: ja
• Article Type: conference paper
• Data Source:
  • IRDB
  • CiNii Articles
  • KAKEN