2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み
Bibliographic Information
- Other Title
-
- 2 リテラル カンシホウ デ ジッソウ サレタ SAT ソルバ エ ノ キホン タイショウセツ ショリ キノウ ノ クミコミ
- Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme
Search this article
Abstract
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
Journal
-
- 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
-
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 111 (268), 67-72, 2011-10
一般社団法人電子情報通信学会
- Tweet
Keywords
Details 詳細情報について
-
- CRID
- 1050845763734805376
-
- NII Article ID
- 110008900205
-
- NII Book ID
- AA1123312X
-
- HANDLE
- 2237/23546
-
- NDL BIB ID
- 023343877
-
- ISSN
- 09135685
-
- Text Lang
- ja
-
- Article Type
- journal article
-
- Data Source
-
- IRDB
- NDL
- CiNii Articles
- KAKEN