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