
                        UnitWalk -- USER MANUAL

Contents:

0. Disclaimer.
1. Introduction.
2. Compilation.
3. Using the program.
4. References and contacts.
Appendix A. DIMACS cnf format.
Appendix B. Format of the output (SATCompetition version).
Appendix C. Format of the output file (normal version).
Appendix D. Name of the output file (normal version).

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

0. Disclaimer.

This documentation typically corresponds to one of the previous versions.

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

1. Introduction.

UnitWalk is an implementation of an incomplete algorithm, that attempts to find a 
satisfying assignment for a Boolean formula in conjunctive normal form. 
It accepts formulas in DIMACS cnf form. 

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

2. Compilation.

Compile UnitWalk by typing "make" in the directory containing this file.  

If you want use non-SATCompetition version type "make normal" in the same 
directory.

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

3.0. Using the program (SATCompetition version).

Type
 
 ./UnitWalk file.cnf 1234

to apply the algorithm to file.cnf containing the input formula, with the 
second parameter as random seed. 

Similarly to other probabilistic SAT solvers, UnitWalk uses random seed
to start its random number generator.

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

3.1. Using the program (normal version).

Type

 ./UnitWalk -f file.cnf
 
 to apply the algorithm to file.cnf containing the input formula.
 The output will go to the screen (can be turned off by the key -q)
 and to the subdirectory Outputs; the name of output file is
 generated automatically from the parameters
 (can be changed by the key -o file).
 
 Another common use is applying the algorithm to the whole directory
 containing .cnf files:
 
  ./UnitWalk -d dirname
  
  A useful key -q makes execution quiet and must be used when
  estimating the running time.
  
  To get a list of all command line options, type
  
   ./UnitWalk -h
   
Similarly to other probabilistic SAT solvers, UnitWalk uses random seed
to start its random number generator. By default it
is 28120107. You can set seed with command line option
"-s your_number" or use random seed with "-sr".

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

4. References.

The last version of UnitWalk typically resides at

http://logic.pdmi.ras.ru/~arist/UnitWalk/

The algorithm is described in the paper

 E. A. Hirsch, A. Kojevnikov, UnitWalk: A new SAT solver that uses local
 search guided by unit clause elimination. Electronic proceedings of SAT-2002.
 http://gauss.ececs.uc.edu/Conferences/SAT2002/sat2002list.htm		   

Questions or comments regarding the program and the algorithm
can be addressed to the authors:

Edward A. Hirsch <http://logic.pdmi.ras.ru/~hirsch>
Arist Kojevnikov <http://logic.pdmi.ras.ru/~arist>

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

Appendix A. DIMACS cnf format.

An input file starts with comments (each line starts with c).
The number of variables and the number of clauses is defined by the line

p cnf variables clauses

Each of the next lines specifies a clause: a positive literal
is denoted by the corresponding number, and a negative literal
is denoted by the corresponding negative number. The last number
in a line should be zero. For example,

c A sample .cnf file.
p cnf 3 2
1 -3 0
2 3 -1 0

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

Appendix B. Format of the output (SATCompetition version).

The output may contain several lines of different 
categories according to their first chars.

  comments - beginning with the 2 chars "c "
  solution - beginning with the 2 chars "s " and one of the following ones:
    s SATISFIABLE
    s UNKNOWN
  values of a solution - beginning with the 2 chars "v " parts of 0-terminated
                         sequence of distinct non-contradictory literals
			 that make every clause of the input formula true

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

Appendix C. Format of the output file (normal version).

The output file may contain several blocks of the form

f <name of the input file> v <satisfying assignment>
<various data on the execution: elapsed time, the number of flips etc.>

and the line "end" after the last one.

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

Appendix D. Name of the output file (normal version).

The name of the output file (if it is not defined by the user) is
automatically generated in the following way:

V<number of version>.<name of the input file>.f.{r<number of restarts>}.
{I<max number of runs>}.{T<max time of execution>}.
{A<max number of assignments>}.s<seed>.pid<process id>
