We would like to explain the discrepency between the data of BerkMin's performance reported in our DATE-2002 paper and in the results of the competition at SAT-2002. In the proceedings of DATE-2002 we described a SAT-solver BerkMin56 (56 is our internal numbering). In the competition of SAT-2002 we used version BerkMin62 which has not been published yet. Our experiments show that BerkMin62 is faster than BerkMin56.

BerkMin56 and BerkMin62 were developed under Microsoft Windows and then ported to Solaris. BerkMin62 has never crashed under Solaris. Unfortunately, running BerkMin62 under Linux exposed a bug. This bug was not found in the "zero" stage of the competition (that was meant for exposing bugs) for the following reason. BerkMin62 consists of two SAT-engines interacting with each other. One of them is BerkMin56 while the other is a new more powerful engine that was meant to be used for large CNF formulas. This new engine actually contained a bug that got exposed only under Linux. Since all the formulas used at the "zero" stage were small they were solved only by BerkMin56 withougt calling the new SAT-engine.

We became aware of the existence of a bug only after the first stage results had been published. According to the information provided by Laurent Simon, BerkMin crashed on 124 formulas (i.e.124 is the number of formulas on which the new buggy SAT-engine was called.) For each crashed instance BerkMin was charged 2400 sec, which was the time limit at the first stage. For instance, in our DATE-2002 paper we report that BerkMin solves the whole family Velev's instances sss.1.0 in 13.4 seconds. On the other hand,according to the results of the competition (first stage) BerkMin was not able to compete 2dlx_cc_mc_ex_bp_f2_bug015 and 2dlx_cc_mc_ex_bp_f2_bug019 in 40 minutes (in reality it just immediately crashed on these two instances).

Even though BerkMin crashed on half the instances it was able to made it to the second (final) stage of the competition in four out of six categories. We started looking for a bug (and quickly found it) immediately after the results of the first stage had been released.Unfortunately, according to the rules of the competition we were not allowed to replace the buggy version of BerkMin62 and so we had to use it in the second stage as well. Nevertheless, BerkMin was able to win competiton in the category of hand-made satisfiable instances!!