Edward A. Hirsch: SAT solvers and benchmarks
Arist Kojevnikov and myself
wins SAT Competition 2003 category "all solvers on
randomly generated satisfiable benchmarks";
Generator hgen8 of random formulas
generated the smallest unsatisfiable instance
that remained unsolved during SAT Competitions 2003 and 2004;
Generator hgen2 of random formulas
generated the smallest satisfiable instance
that remained unsolved during SAT Competition 2002.
Curiously, even smaller benchmarks generated by this generator
remained unsolved during SAT Competitions 2003, 2004.
Mixed Boolean-Algebraic Solver, developed by our team under Intel support through CRDF grant.