MAX-2-SAT instances

The files in this directory are MAX-2-SAT instances partially tested in the
following papers.

  Y. Koga, M. Yagiura, K. Nonobe, T. Imamichi, H. Nagamochi and T. Ibaraki,
    Efficient branch-and-bound algorithms for weighted MAX-2-SAT,
    Proceedings of the Third International Conference on Innovative
    Applications of Information Technology for Developing World
    (Asian Applied Computing Conference (AACC 2005)),
    Kathmandu, Nepal, December 10-12, 2005.

  Y. Koga, Efficient branch-and-bound algorithms for weighted MAX-2-SAT,
    Master thesis, Department of Applied Mathematics and Physics,
    Graduate School of Informatics, Kyoto University, 2006.


The format is as follows:
 the first line: "p cnf" #variables, #clauses;
 for each clause: weight, literal, literal, "0"
 (negation is represented by minus).


The first part of file names represents the type of the instance:
  uBF, wBF - random instances generated by Borchers & Furman,
  urand, wrand - random instances generated by us,
  break - instances from the break minimization problem by Miyashiro & Matsui,
  cut, bal - hard instances generated by Tavares,
  reg - instances from regular graphs generated by us.
For uBF, wBF, urand and wrand, "u" and "w" represent "unweighted" and
"weighted", respectively.

Except for type "break", names are in the form of

  "(type)_(#variables)_(#clauses).wcnf",

while for type "break", names are in the the form of

  "(type)_(#teams)_(#variables)_(#clauses).wcnf".

Files "chart*.dat" are matching tables of instances of the break minimization
problem.

Instances of uBF and wBF were taken from the following web page.
http://infohost.nmt.edu/~borchers/maxsat.html

Instances of urand and wrand were generated by using "mwff" generator, which
is available at the following site.
ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/cotributed/selman/


Note:
Until February 2006, we had instances whose names start with "p2" or "wp2"
in this directory. This note is for those who had downloaded them and tested 
for comparisons. In order to clarify the instance types, we changed their
names to "urand" and "wrand", respectively. If the sizes are the same (e.g., 
p2_50_200.wcnf and urand_50_200.wcnf), they are exactly the same.

all instances (tar + bzip2)