DIMACS Challenge II: June 9, 1993 Update There are a number of interesting files newly available at the Challenge ftp site (dimacs.rutgers.edu, all in the pub/challenge subdirectory). These include: sat/contributed/UCSC/parser/: parser from Allen Van Gelder (avg@cs.ucsc.edu). This code formalizes the structure of the cnf format. sat/translators/: codes to translate from cnf format to sat format, and from conjunctive normal form expressions in sat format to cnf format by Tamas Badics (badics@rutcor.rutgers.edu). graph/contributed/pardalos/*.f: A number of interesting generators for clique problems from Panos Pardalos (pardalos@math.ufl.edu). sat/contributed/dubois/gensathard.c: generator from Olivier Dubois (dubois@laforia.ibp.fr) that generates hard sat problems. sat/contributed/barth: Implementation of Davis Putnam from Peter Barth (barth@mpi-sb.mpg.de), including many heuristic additions. graph/contributed/lewandowski: generators and test problems for coloring register allocation graphs from Gary Lewandowski (gary@cs.wisc.edu). This is a "shar" file, which, after expansion, includes a test directory with sample coloring instances. sat/contributed/stamm-wilbrandt/IAI-TR-93-3.ps: A technical report from Hermann Stamm-Wilbrandt (hermann@holmium.informaik.uni-bonn.de) that gives a number of reductions from hard and easy problems to satisfiability. These reductions might be an interesting source of instances. I am still putting together some benchmark problems, so feel free to pass along your favorite instances. Mike Trick Carnegie Mellon University/ Challenge Coordinator