Fifty-Five Solvers in Vancouver: The SAT 2004 Competition

Overview & Synopsis

For the third consecutive year, a SAT competition was orga- nized as a joint event with the SAT conference. With 55 solvers from 25 author groups, the competition was a clear success. One of the noticeable facts from the 2004 competition is the superiority of incomplete solvers on satisfiable random k-SAT benchmarks. It can also be pointed out that the complete solvers awarded this year, namely Zchaff, jerusat1.3, satzoo-1.02, kncfsand march-eq, participated in the SAT 2003 com- petition (or at least former versions of those solvers). This paper is not reporting exhaustive competition results, already available in details on- line, but rather focuses on some remarkable results derived from the competition dataset. The SAT 2004 competition is ending a 3-year take-off period that at- tracted new SAT researchers and provided many new benchmarks and solvers to the community. The good participation rate of this year (de- spite the addition of the anti-blackbox rule) establishes the competition as an awaited yearly event. Some new directions for a new way of thinking about the competition are discussed at the end of the paper.