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