Edward A. Hirsch I am a theoretical computer scientist (that is, mathematician) interested in computational complexity and proof theory. News: CSR-2018 will be held in Moscow in June 2018.

Research papers Teaching Students Affiliations, committees... SAT tools Addresses 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]