FILES & THE INSTANCE ----------------------------------------------------------

The files in this directory are the MAXSAT instance called TTP 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).

Some related files are also included.

The instance used in this paper is in file "TimeTable2w-1.sat", whose format
is the same as the random instances such as "rndw1000a01", i.e.,

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

This time tabling instance was originally used in

  S. Miyazaki, K. Iwama and Y. Kambayashi,
  Database Queries as Combinatorial Optimization Problems,
  Proc. International Symposium on Cooperative Database Systems for 
  Advanced Applications (CODAS'96), pp. 448-454, 1996 (Kyoto, Japan),

where its MAXSAT formulation was slightly different from "TimeTable2w-1.sat"
(the weights on clauses are different). The details of the original time
tabling instance and the transformation to MAXSAT are found in this paper.
This instance was also tested in the following papers.

  B. Cha, K. Iwama, Y. Kambayashi and S. Miyazaki,
  Local Search Algorithms for Partial MAXSAT,
  Proceedings of the 14th National Conference on Artificial Intelligence
  and 9th Innovative Applications of Artificial Intelligence Conference
  (AAAI 97), pp. 263-268, 1997.

  K. Iwama, D. Kawai, S. Miyazaki, Y. Okabe and J. Umemoto,
  Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM,
  Proc. Workshop on Algorithm Engineering (WAE 2000), (Lecture Notes in
  Computer Science 1982), pp. 123-134, Sept., 2000. (Saarbrucken, Germany).
  
  K. Iwama, D. Kawai, S. Miyazaki, Y. Okabe and J. Umemoto,
  Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM,
  The ACM Journal of Experimental Algorithmics, Volume 7, Article 2, 2002.

  K. Nonobe and T. Ibaraki,
  An improved tabu search method for the weighted constraint satisfaction problem,
  INFOR, Vol. 39, pp. 131-151, 2001. 



EVALUATION --------------------------------------------------------------------

Before evaluating solutions, compile "evalsol.c" by, e.g.,

  gcc -O2 -o evalsol evalsol.c

A solution should be stored in a file in the following format:

  for each variable x_1, x_2, ..., x_n, in this order,
  write their values in 0 or 1 (0 = false, 1 = true)
  with at least one space between two values.

The file "sample_sol" is a sample in this format (the best solution obtained
by the ILS). Then, to evaluate a solution, type

  cat data sample_sol | ./evalsol

Then the number of unsatisfied constraints are printed as follows.

   # number of unsatisfied clauses:
    for step1:   0
    for step2:   0
    for step3:   0
    for step4:  85
    for step5:   0
    for step6:   0
   	total:  85

Constraints of steps 1 through 3 are hard, i.e., if you have nonzero in the
first three lines, then your time table is infeasible, unfortunately.
Constraints of steps 4 through 6 are soft, and the solutions are evaluated
by the total of these three values (i.e., the last line named "total").


WEIGHTS FOR CLAUSES -----------------------------------------------------------

The results will be affected by the weights of the clauses, and you can
generate instances with different weights for the clauses by appropriately
modifying "gendata.c".

Usage:
  gcc -O2 -o gendata gendata.c
  cat data | ./gendata > TimeTable.sat

-------------------------------------------------------------------------------