Edward A. Hirsch I am a theoretical computer scientist (that is, mathematician) interested in computational complexity and proof theory. News: CSR-2021 will be held in Sochi, deadline December 24, 2020. In 2022, CSR will be an ICM satellite!

Research papers Teaching Students Affiliations, committees... SAT tools Contacts Personal

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.

[Laboratory] [Institute]