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

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)33-39
Number of pages7
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume12
Issue number1
Publication statusPublished - Mar 1 2007

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Cite this

Implementation of a SAT solver Herrsat in Java and a method for eliminating learned clauses. / Omori, Shinsaku; Matsushita, Konosuke; Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki.

In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 12, No. 1, 01.03.2007, p. 33-39.

Research output: Contribution to journalArticle

@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 = "3",
day = "1",
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, Faculty of Science",
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/1

Y1 - 2007/3/1

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 - http://www.scopus.com/inward/record.url?scp=34548012877&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34548012877&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:34548012877

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

SN - 1342-3819

IS - 1

ER -