書誌事項
- タイトル別名
-
- 2 リテラル カンシホウ デ ジッソウ サレタ SAT ソルバ エ ノ キホン タイショウセツ ショリ キノウ ノ クミコミ
- Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme
この論文をさがす
抄録
論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.そこで, Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,そのままでは高速化が期待できない.本論文では,通常の節(OR節)は二つのリテラルを監視し,基本対称節については節中のリテラルをすべて監視する方法を提案する,実際にこれをMinisatに組み込むことで,本手法の有効性を評価する.
収録刊行物
-
- 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
-
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 111 (268), 67-72, 2011-10
一般社団法人電子情報通信学会
- Tweet
キーワード
詳細情報 詳細情報について
-
- CRID
- 1050845763734805376
-
- NII論文ID
- 110008900205
-
- NII書誌ID
- AA1123312X
-
- HANDLE
- 2237/23546
-
- NDL書誌ID
- 023343877
-
- ISSN
- 09135685
-
- 本文言語コード
- ja
-
- 資料種別
- journal article
-
- データソース種別
-
- IRDB
- NDL
- CiNii Articles
- KAKEN