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.