The files in this directory are MAXSAT instances tested in 

  M. Yagiura and T. Ibaraki,
  "Efficient 2 and 3-Flip Neighborhood Search Algorithms for the MAX SAT:
  Experimental Evaluation," Journal of Heuristics, Vol. 7, pp. 423-442, 2001.
  (http://www-or.amp.i.kyoto-u.ac.jp/~yagiura/papers/msatexp97_abst.html).

Instance types:
 rndw1000a01 ... rndw1000a10: RNDW instances of n=1000 & m=7700
 rndw1000b01 ... rndw1000b10: RNDW instances of n=1000 & m=11050
 rg_200_2000_4_xx: GCP instances of n=800 & m=8200

The format is:
 the first line: #variables, #clauses;
 for each clause: #literals, weight, literal, literal, ...
  (negation is represented by minus).

To generage CNF format:
 COMPILE
  % gcc -O2 -o msat2cnf msat2cnf.c
 USAGE
  % cat rndw1000b01 | msat2cnf keepweight 1

By the option "keepweight 1", weights are represented by duplicating clauses.

To get RNDU (unweighted) instances:
 COMPILE
  % gcc -O2 -o cnf2msat cnf2msat.c
 USAGE
  % cat rndw1000b01 | msat2cnf keepweight 0 | cnf2msat      (maxsat format)
  % cat rndw1000b01 | msat2cnf keepweight 0                 (CNF format)