| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 419040 | Discrete Applied Mathematics | 2007 | 13 Pages |
Abstract
We describe a SAT-solver, BerkMin, that inherits such features of GRASP, SATO, and Chaff as clause recording, fast BCP, restarts, and conflict clause “aging”. At the same time BerkMin introduces a new decision-making procedure and a new method of clause database management. We experimentally compare BerkMin with Chaff, the leader among resolution-based SAT-solvers. Experiments show that our program is more robust than Chaff being able to solve more instances than Chaff in a reasonable amount of time.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Eugene Goldberg, Yakov Novikov,