Edward A. Hirsch: SAT solvers and benchmarks

• Solver UnitWalk by 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 hgen8-n260-01...cnf that remained unsolved during SAT Competitions 2003 and 2004;
• Generator hgen2 of random formulas generated the smallest satisfiable instance hgen2-v500-s1216665065.cnf 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.