
                        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.

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

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.  

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

3. Using the program.

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.
-----------------------------------------------------------------------------

4. References.

The last version of UnitWalk typically resides at

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

The algorithm is described in the paper

Edward A. Hirsch, Arist Kojevnikov,
"Solving Boolean satisfiability using local search guided by 
unit clause elimination", Proceedings of CP'01 (to appear).

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

Edward A. Hirsch <hirsch@pdmi.ras.ru>
Arist Kojevnikov <arist@logic.pdmi.ras.ru>

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

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.

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-contraditory literals
			 that make every clause of the input formula true

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

