| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2011-10-28 12:15 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み ○日野善信・酒井正彦・坂部俊樹・草刈圭一朗・西田直樹（名大）  SS2011-38 |
|
| 抄録 | （和） | 論論理式の充足可能性判定問題（SAT問題）を解くSATソルバの高速化の一手法として，馬野らは2010年にCNFへの基本対称節の導入を提案した． 彼らのSATソルバは，節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある． そこで，Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法（２リテラル監視法）に基づく実現が可能であれば，バックトラックが軽くなるため更なる高速化が期待できる． しかしながら，基本対称節の性質から二つのリテラルのみの監視では十分でなく， そのままでは高速化が期待できない． 本論文では，通常の節（OR節）は二つのリテラルを監視し，基本対称節については節中のリテラルをすべて監視する方法を提案する． 実際にこれをMinisatに組み込むことで，本手法の有効性を評価する． |
| （英） | Umano et al.\ introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SAT-solver efficiency. Since their experimental SAT solver is implemented based on two counters that maintain the number of true (false, respectively) literals, it has a drawback that backtracks are heavy. Thus much faster solvers are expected due to light backtracks if it is possible to implement them based on watching two literals for each clause, called two watched literals adopted by modern SAT solvers like Minisat. However, watching two literals for ES-clauses are not enough for efficiency. This paper proposes a method watching two literals for each ordinary clause and watching all literals for each ES-clause, and evaluates this by incorporating it into Minisat. |
|
| キーワード | （和） | SATソルバ / 基本対称節 / ２リテラル監視法 / 全リテラル監視法 / / / / |
| （英） | SAT Solver / Elementary Symmetric Clauses / Two Watched Literals / All Watched Literals / / / / | |
| 文献情報 | 信学技報, vol. 111, no. 268, SS2011-38, pp. 67-72, 2011年10月. | |
| 資料番号 | SS2011-38 | |
| 発行日 | 2011-10-20 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2011-38 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2011-10-27 - 2011-10-28 |
| 開催地（和） | 北陸先端科学技術大学院大学 |
| 開催地（英） | JAIST |
| テーマ（和） | 一般 |
| テーマ（英） | General topics |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2011-10-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み |
| サブタイトル（和） | |
| タイトル（英） | Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme |
| サブタイトル（英） | |
| キーワード(1)（和/英） | SATソルバ / SAT Solver |
| キーワード(2)（和/英） | 基本対称節 / Elementary Symmetric Clauses |
| キーワード(3)（和/英） | ２リテラル監視法 / Two Watched Literals |
| キーワード(4)（和/英） | 全リテラル監視法 / All Watched Literals |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 日野 善信 / Yoshizane Hino / ヒノ ヨシザネ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2011-10-28 12:15:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2011-38 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | no.268 |
| ページ範囲 | pp.67-72 |
| ページ数 | 6 |
| 発行日 | 2011-10-20 (SS) |
[研究会発表申込システムのトップページに戻る]