|BerkMin is a propositional 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 (on the left) or Yakov Novikov (on the right)|
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.