## Welcome to BerkMin's web page

### What is BerkMin?

### 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:
- better optimized code;
- better tuned heuristics;
- faster input of CNF formulas;
- possibility of choosing between several strategies of decision making and restart policies;
- possibility of tuning the program to the size of the formula

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.