@article{oai:nagoya.repo.nii.ac.jp:00021402,
 author = {日野, 善信 and 酒井, 正彦 and 坂部, 俊樹 and 草刈, 圭一朗 and 西田, 直樹 and HINO, Yoshizane and SAKAI, Masahiko and SAKABE, Toshiki and KUSAKARI, Keiichirou and NISHIDA, Naoki},
 issue = {268},
 journal = {電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス},
 month = {Oct},
 note = {論理式の充足可能性判定問題(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., IEICE Technical Report;SS2011-38},
 pages = {67--72},
 title = {2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み},
 volume = {111},
 year = {2011}
}