講演抄録/キーワード |
講演名 |
2011-10-28 12:15
2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み ○日野善信・酒井正彦・坂部俊樹・草刈圭一朗・西田直樹(名大) SS2011-38 |
抄録 |
(和) |
論論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.
彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.
そこで,Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.
しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,
そのままでは高速化が期待できない.
本論文では,通常の節(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ソルバ / 基本対称節 / 2リテラル監視法 / 全リテラル監視法 / / / / |
(英) |
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 |