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

Intelligence Science

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	33-39
Number of pages	7
Journal	Research Reports on Information Science and Electrical Engineering of Kyushu University
Volume	12
Issue number	1
Publication status	Published - Mar 2007

All Science Journal Classification (ASJC) codes

General Computer Science
Electrical and Electronic Engineering

Cite this

@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

Abstract

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this