WEKO3
アイテム
SATソルバーの使い方---問題をSATに符号化する方法---
https://ipsj.ixsq.nii.ac.jp/records/222481
https://ipsj.ixsq.nii.ac.jp/records/222481df6d5c63-6912-4d64-b2bc-88ae034237d6
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2017023.pdf (366.3 kB)
|
Copyright (c) 2017 by the Information Processing Society of Japan
|
| Item type | Symposium_02(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2017-01-06 | |||||||||
| タイトル | ||||||||||
| タイトル | SATソルバーの使い方---問題をSATに符号化する方法--- | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | How to use SAT solvers---How to encode problems to SAT--- | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | SATソルバー，SAT符号化，制約モデル | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||
| 資源タイプ | conference paper | |||||||||
| 著者所属 | ||||||||||
| 神戸大学 情報基盤センター;;神戸大学 情報基盤センター;;神戸大学 情報基盤センター | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Information Science and Technology Center, Kobe University;;Information Science and Technology Center, Kobe University;;Information Science and Technology Center, Kobe University | ||||||||||
| 著者名(英) |
田村, 直之 宋 剛秀 番原 睦則
× 田村, 直之 宋 剛秀 番原 睦則
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | SATソルバーは，与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである．Knuthによる著名な教科書 The Art of Computer Programming の最新分冊では，300ページ以上もの分量がSATソルバーとその応用の説明に割かれ，最近のホットなトピックの一つとなっている．このようなSATソルバーの発展を背景とし，解きたい問題をCNF式に変換(SAT符号化)しSATソルバーで解を求める手法が注目されている．しかし，解きたい問題が複雑な場合，それを直接SAT符号化することはかなり面倒な仕事だ．代わりに，まず与えられた問題を整数変数上の制約モデルとして定式化し，次にその制約モデルのSAT符号化を考える方法が有効である．そこで，本発表では上記のKnuthの教科書でも取り上げられている例題を題材とし，制約モデル・SAT符号化の選択肢について説明・比較を行い，SATソルバーをより有効に利用する方法を紹介する． | |||||||||
| 書誌情報 | 巻 2017, p. 165-172 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
