Although these appeared 20 years ago, they still continue to attract attention.

• 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, 2005.

Also you may want to check the web page of my SAT course.