Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses

Shinsaku Omori; Konosuke Matsushita; Ryuzo Hasegawa; Hiroshi Fujita; Miyuki Koshimura

Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses

Shinsaku Omori
, Konosuke Matsushita
, Ryuzo Hasegawa
, Hiroshi Fujita
, Miyuki Koshimura

知能科学

研究成果: ジャーナルへの寄稿 › 学術誌 › 査読

抄録

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.

本文言語	英語
ページ（範囲）	33-39
ページ数	7
ジャーナル	Research Reports on Information Science and Electrical Engineering of Kyushu University
巻	12
号	1
出版ステータス	出版済み - 3月 2007

!!!All Science Journal Classification (ASJC) codes

コンピュータサイエンス一般
電子工学および電気工学

他のファイルとリンク

引用スタイル

@article{a1a8db5432da4328b1b7df230607ce4e,

title = "Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses",

abstract = "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.",

author = "Shinsaku Omori and Konosuke Matsushita and Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura",

year = "2007",

month = mar,

language = "English",

volume = "12",

pages = "33--39",

journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",

issn = "1342-3819",

publisher = "Kyushu University",

number = "1",

}

TY - JOUR

T1 - Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses

AU - Omori, Shinsaku

AU - Matsushita, Konosuke

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

AU - Koshimura, Miyuki

PY - 2007/3

Y1 - 2007/3

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/34548012877

UR - https://www.scopus.com/pages/publications/34548012877#tab=citedBy

M3 - Article

AN - SCOPUS:34548012877

SN - 1342-3819

VL - 12

SP - 33

EP - 39

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

IS - 1

ER -

Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses

抄録

!!!All Science Journal Classification (ASJC) codes

他のファイルとリンク

フィンガープリント

引用スタイル