How to Install and Run SATO (version 3.2)
             -----------------------------------------
This version fixed some bugs in the previous version.
The rest of the README file is the same as for the previous one.

SATO stands for "SAtisfiability Testing Optimized".
This file contains instructions to install sato, a decision procedure
for propositional logic written in C by Hantao Zhang.

1. Download the file sato4.1.tgz and put the file into your directory.

2. Extract the Files:

% tar xvfz sato4.1.tgz

The following files will be generated:

clocks.h  main.h    proto.h  sato.c  select.h  tape.h  weight.h
main.c    makefile  santo.h  sato.h  stack.h   util.c

3. Install Sato:

% make
The following messages will appear on a SGI workstation:

gcc -O3 -DQUASICLAUSE   -c -o main.o main.c
gcc -O3 -DQUASICLAUSE   -c -o sato.o sato.c
gcc -O3 -DQUASICLAUSE   -c -o util.o util.c
gcc -O3 -DQUASICLAUSE main.o sato.o util.o -lc -o sato
chmod a+x sato

4. Run Sato:

A simple online instruction is given when sato is typed:

% ./sato
Usage: sato <Input_file> [<Options>]

Options are:
   -e fname : give the file name of unfinished jobs (default: unfinish)
   -g<n>    : set the amount of space for lemmas (default: 5)
   -h<n>    : set the number of hours to be run (default: 47)
   -m<n>    : set the number of minutes to be run (default: 0)
   +m<n>    : set the number of expected models (default: 1)
   -n       : rename variable names to make name space compact
   -t       : do not print models

Input_file is a file name. The input consists of a list of clauses, each of
    which is a list of nonzero integers separated by 0 (DIMACS Format).

    Example: To input clauses p1|p2, -p1|p3|p4, and p2|-p3|p4 in
       DIMACS Format, please prepare a file whose content is as follows:
       
       c This is a simple example with 3 clauses and 
       c 4 variables. Each literal is represented by an integer
       c and each clause ends with 0.
       c The line below is the header of DIMACS format.
       p cnf 4 3
       1 2 0   
       -1 3 4 0
       2 -3 4 0

    Tautologies and duplicated literals are always removed by sato.
    E.g., (1 1 -2 -4) is the same as (1 -2 -4).

6. Report Problems to:

      hzhang@cs.uiowa.edu 
or
      Hantao Zhang
      Department of Computer Science 
      University of Iowa
      Iowa City, Iowa 52242