WEKO3
-
RootNode
アイテム
SAT技術の進化と応用 〜パズルからプログラム検証まで〜:2.SATとパズル -問題をいかにSATソルバーで解くか-
https://ipsj.ixsq.nii.ac.jp/records/169443
https://ipsj.ixsq.nii.ac.jp/records/169443df66b3c8-244f-4471-b227-88c5bced93ce
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 2016 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Magazine(1) | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|
公開日 | 2016-07-15 | |||||||||||
タイトル | ||||||||||||
タイトル | SAT技術の進化と応用 〜パズルからプログラム検証まで〜:2.SATとパズル -問題をいかにSATソルバーで解くか- | |||||||||||
タイトル | ||||||||||||
言語 | en | |||||||||||
タイトル | SAT Evolution and Applications:2. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver - | |||||||||||
言語 | ||||||||||||
言語 | jpn | |||||||||||
キーワード | ||||||||||||
主題Scheme | Other | |||||||||||
主題 | 特集 | |||||||||||
資源タイプ | ||||||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||||
資源タイプ | article | |||||||||||
著者所属 | ||||||||||||
神戸大学 | ||||||||||||
著者所属 | ||||||||||||
神戸大学 | ||||||||||||
著者所属 | ||||||||||||
神戸大学 | ||||||||||||
著者所属(英) | ||||||||||||
en | ||||||||||||
Kobe Univ. | ||||||||||||
著者所属(英) | ||||||||||||
en | ||||||||||||
Kobe Univ. | ||||||||||||
著者所属(英) | ||||||||||||
en | ||||||||||||
Kobe Univ. | ||||||||||||
著者名 |
田村, 直之
× 田村, 直之
× 宋, 剛秀
× 番原, 睦則
|
|||||||||||
著者名(英) |
TAMURA, Naoyuki
× TAMURA, Naoyuki
× SOH, Takehide
× BANBARA, Mutsunori
|
|||||||||||
論文抄録 | ||||||||||||
内容記述タイプ | Other | |||||||||||
内容記述 | 数独やナンバーリンクなどのパズルを題材として取り上げ,SATソルバーを用いてこれらのパズルを解く方法について説明する.SATソルバーは,与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである.近年になって大幅な性能向上が実現され,最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている.このことを背景とし,さまざまな問題をCNF式に変換(符号化) しSAT ソルバーで解を求める手法が注目を集めている.本稿では,パズルを題材とすることで,この手法について分かりやすく解説する. | |||||||||||
書誌レコードID | ||||||||||||
収録物識別子タイプ | NCID | |||||||||||
収録物識別子 | AN00116625 | |||||||||||
書誌情報 |
情報処理 巻 57, 号 8, p. 710-715, 発行日 2016-07-15 |
|||||||||||
出版者 | ||||||||||||
言語 | ja | |||||||||||
出版者 | 情報処理学会 |