著者
田村 直之 宋 剛秀 番原 睦則
雑誌
情報処理
巻号頁・発行日
vol.57, no.8, pp.710-715, 2016-07-15

数独やナンバーリンクなどのパズルを題材として取り上げ,SATソルバーを用いてこれらのパズルを解く方法について説明する.SATソルバーは,与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである.近年になって大幅な性能向上が実現され,最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている.このことを背景とし,さまざまな問題をCNF式に変換(符号化) しSAT ソルバーで解を求める手法が注目を集めている.本稿では,パズルを題材とすることで,この手法について分かりやすく解説する.

言及状況

はてなブックマーク (1 users, 1 posts)

Twitter (1 users, 1 posts, 1 favorites)

収集済み URL リスト