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.
|Number of pages
|Research Reports on Information Science and Electrical Engineering of Kyushu University
|Published - Mar 2007
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering