Welcome to BerkMin's web page

What is BerkMin?

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)
Berkeley Minsk

BerkMin561 (The only publicly available version of BerkMin. Released at the beginning of 2003)

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.

To download BerkMin561

click here




SAT-2004 competition

We didn't enter any new version of BerkMin in SAT-2004 . The only our program that took part in SAT-2004 was an old version of Forklift (it automatically entered the competition as a winner of SAT-2003). Forklift was not allowed to enter the second stage of the competition (probably, because of the "black box" rule.) Jerusat1.3 and Zchaff_rand were declared winners in the industrial category. At the first stage of the competition, in the industrial category, Jerusat1.3. solved 56 formulas from 21 benchmark sets, Zchaff_rand solved 67 formulas from 27 benchmark sets and Forklift solved 81 formulas from 30 benchmark sets.

SAT-2003 competition

BerkMin561 and our other SAT-solver Forklift took part in the SAT-2003 competition . Forklift became the winner in both categories of industrial benchmarks ("satisfiable" and "satisfiable+unsatisfiable"). BerkMin561 came in second. Forklift is a derivative of BerkMin that has an auxiliary learning technique (in addition to regular conflict based learning).

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.