-------------------------------------------------------------------------------
Program Codes.

Files in "msat.tar.gz" are the program codes in C used in the following papers:

  - M. Yagiura and T. Ibaraki, "Analyses on the 2 and 3-Flip Neighborhoods
    for the MAX SAT," Journal of Combinatorial Optimization, Vol. 3, No. 1,
    pp. 95-114, July 1999. 

  - M. Yagiura and T. Ibaraki, "Efficient 2 and 3-Flip Neighborhood Search
    Algorithms for the MAX SAT: Experimental Evaluation," Journal of
    Heuristics, Vol. 7, No. 5, pp. 423-442, 2001.

  - M. Yagiura and T. Ibaraki, "On Metaheuristic Algorithms for Combinatorial
    Optimization Problems," Systems and Computers in Japan, Vol. 32, Issue 3,
    2001, pp. 33-55.
    (The translation of the following paper: M. Yagiura and T. Ibaraki, "On
    Metaheuristic Algorithms for Combinatorial Optimization Problems (in
    Japanese)", The Transactions of the Institute of Electronics, Information
    and Communication Engineers, Vol. J83-D-I, No.1, pp. 3-25, Jan. 2000).

To extract program files, type as follows.

  % tar zxvf msat.tar.gz

Then a directory "msat" is made and program codes are extracted under it.
The correspondence of directories and algorithms are as follows.

  gls/		genetic local search (GLS)
  grasp/	GRASP (greedy randomized adaptive search procedure)
  ils/		iterated local search (ILS)
  mlsf/		random multi-start local search (MLS)
  sa/		simulated annealing (SA) and threshold accepting (TA)
  tabu/		tabu search (TS)

To compile them, just type "make" under each directory. Note that two
executable files, "sasat" and "tasat" will be made under directory "sa".

To run the algorithms, type, e.g., as follows (in the case of tabu search).

  % gunzip -c rndw1000a01.gz | ./tabusat
  % ./tabusat < rndw1000a01

You can change various parameters from the command line, e.g., by typing
as follows. 

  % gunzip -c rndw1000a01.gz | ./tabusat timelim 1 ttenure 10

Most parameters defined in "#define" lines, e.g.,

  #define TTENURE         20      /* tabu tenure */

can be changed from the command line in this way. Note that you have to
use small letters (e.g., "TTENURE" in the #define line must be changed
to "ttenure" in the command line).

NOTE: These program codes are not very sophisticated and you have to adjust
 their parameter values to make them work properly. That is, they can be very
 sensitive to their parameter values. As for MLS, ILS and TS, you can get some
 information on their behavior against important parameters from the above
 mentioned paper in Journal of Heuristics.

-------------------------------------------------------------------------------
Filters.

msat2cnf.c and cnf2msat.c are filters to change the format of instances.

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)

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