作成者 |
|
|
|
|
|
本文言語 |
|
出版者 |
|
|
発行日 |
|
収録物名 |
|
巻 |
|
号 |
|
開始ページ |
|
終了ページ |
|
出版タイプ |
|
アクセス権 |
|
JaLC DOI |
|
関連DOI |
|
関連URI |
|
関連情報 |
|
概要 |
We have developed a SAT solver Herrsat written in Java. Herrsat is based on MiniSat, a state-of-the-art SAT solver written in C++. Most SAT solvers generate 'learned clauses' during solving process in... order to prune search spaces. We built a simplification function, which eliminates unnecessary clauses, into Herrsat. We compare the solving speed of Herrsat with that of MiniSat using some typical problems. We also measure the effect of the simplification function.続きを見る
|