Welcome to BerkMin's web page

A new release of BerkMin56 is available!!!!

What is BerkMin?

BerkMin is our wonderful SAT-solver. The name BerkMin stands for Berkeley-Minsk that are the cities where the authors of BerkMin live. The version of BerkMin that is further referred to as BerkMin56 is described in E.Goldberg, Y.Novikov. BerkMin: a Fast and Robust SAT-Solver. DATE-2002,pp. 142-149 .

If you have any questions drop a line to Eugene Goldberg or Yakov Novikov

BerkMin561 (new version of BerkMin56)

The new release, BerkMin561, is an optimized version of BerkMin56. New features of BerkMin561 are: To convince you that BerkMin561 is indeed faster than BerkMin56 we give a comparision of Zchaff, BerkMin56 and BerkMin561 on second-stage examples from the SAT-2002 competition. This comparison shows that on this set of instances BerkMin56 outperforms Zchaff and BerkMin561 outperforms BerkMin56. We believe that among the SAT-solvers that are currently available in the public domain, for many “real-life” instances, BerkMin561 will be the most efficient program. It has been successfully applied to solving very large CNF formulas (having more than a million variables and a few millions of clauses). Here is a detailed description of the new release and the list of available binaries .

BerkMin561-solaris.gz (a Solaris binary)
BerkMin561-linux.gz (a Linux binary)
BerkMin561-exe.gz (a Cygwin binary)

BerkMin56 (the old version)

We are going to keep the binaries of BerkMin56 at this web site for a while. Here they are.

BerkMin56-Solaris.gz (a Solaris binary)
BerkMin56-Linux.gz (a Linux binary)
BerkMin56-Cygwin.zip (a Cygwin binary)

BerkMin62 (future releases)

Currently we maintain a few versions of BerkMin including BerkMin561 and BerkMin62. In our "internal" research, for large instances from the formal verificaion domain with more than 20,000-25,000 variables we use BerkMin62 (and its descendents). We are going to make BerkMin62 publicly available in the future.

SAT-2002 competition

BerkMin took part in the SAT-2002 competition . Unfortunately, a new version of BerkMin (version 62) that entered the compeition turned out to have a bug. (The bug did not affect the correctness of results. It just made BerkMin crash on almost all large instances. Here is a more detailed explanation of what happened.) Interestingly, even a half-dead BerkMin62 made it to the second (final) stage in 4 out of 6 categories and was the winner in one of them! Our main concern is BerkMin's performance on industrial benchmarks. Here are the results of running the competition version of BerkMin62 (minus the bug mentioned above) on the instances used in the second stage of the two categories of industrial benchmarks ("satisfiable+unsatisfiable" and "only satisfiable" instances). The winner in the "satisfiable+unsatisfiable" category zChaff was able to solve 7 out of 31 instances within the 6-hour time limit. BerkMin solves 14 instances. The winner in the "only satisfiable" category, limmat, solved 2 instances within the same time limit while BerkMin62 solves 4.

However, even though BerkMin62 is, in general, faster than BerkMin56, the performance of the latter on competition benchmarks (in terms of the number of instances solved within the time limit) is almost the same. Actually, BerkMin56 does slightly better than BerkMin62 on the 31 instances mentioned above. It solves (in less than 6 hours) 15 instances versus 14 by BerkMin62.