
dp02.tar.Z

This package contains the ANSI C sources of an implementation of the
well known Davis Putnam procedure for solving propositional satisfiability
problems.
It should compile without any warnings.

The problem description must be in clausal form.
A positive literal is a positive integer, a negative literal
a neg. integer.
A clause is a sequence of literals separated by whitespace or '|' 
A clause ends with '.' and <END OF LINE> (Un*x EOLN).
(Use the option -0 to disallow <END OF LINE> as end of clause and enable
 '0' as end of clause.)
A Problem description ends with 'ENDATA' or <EOF>.
Characters are ignored while scanning the input.
Lines beginning with c,p,* are comments.

HEURISTICS:
  Up to now 6 variable choosing heuristics:
    none 	(-h0) 
	first variable left is chosen positive (default)
    Jeroslow/Wang  (-h1)
	as described in their paper:
	  "Solving propositional satisfiability problems"
	  R.E. Jeroslow and J. Wang
	  Annals of {M}athematics and {AI}
	  Pages 167-187; Volume 1; 1990
    max. number of occurrences (-h2)
	The *variable* with the maximal number of occurrences is selected
	with sign of the maximal number of occurrences with this sign.
    A variant of JW  (-h3)
	We use the same evaluation function as in JW, but we evaluate
	not each literal on its own but the sum of pos. and neg. sign
	as in (h2).
    random (-h4)
	select randomly a literal. At each invocation there should be another
	result as the random number generator is initialized with the current time.
    A variant from h2 (-h5)
	The *variable* with the maximal number of occurrences *in binary clauses*
        is selected with sign of the maximal number of occurrences with this sign.
	If there are several maximal variables use h2.
	This heuristic comes from Andreas Eisele <andreas@adler.ims.uni-stuttgart.de>.
    Another variant of h2 (-h6)
	literal X with max. vector under lexicographic order
	      (H_2(X),H_3(X),....)
	where H_i(X) is
	      1*max(h_i(X),h_i(-X)) + 2*min(h_i(X),h_i(-X))
	where h_i(X) is the number of clauses of length i containing X 
	Idea of heuristic from Max Boehm : 
	boehm@engels1.cs.uni-duesseldorf.de
	

    ****** The heuristics h5 and h6 are described in 
		"Report on a sat competition" , M.Buro, H.Kleine B"uning; 
		FB 17 Mathematik/Informatik Universit"at Paderborn.
		Bericht Nr. 110 ; Reihe Informatik; November 1992
	dp is about 2-10 times slower.
	(It is horribly slow if many small clauses are in the problem.)
	Because the heuristic data needs to be recalculated each time a variable
	is selected this seems to be acceptable.
	(Especially h6 spends a lot of time in selecting a variable).


REMARKS:
  No monotone variable fixing is done.
  The implementation uses some index-datastructure. The memory requirements are
    relatively small. 


INSTALLATION:
1) Uncompress the package
	uncompress dp02.tar.Z
   and untar it in a separate directory
	tar -xvf dp02.tar
   
2) Change Makefile if necessary, then type
	make
   If this doesn't work, then "Good Luck"

3) Test it. (for example)

	mpii02045 [14:45] 51 SAT -> dp -t2 < hole6
	dp version 0.2, Copyright (C) 1993 Peter Barth 
	dp comes with ABSOLUTELY NO WARRANTY; for details look in the file COPYING. 
	This is free software, and you are welcome to redistribute it 
	under certain conditions; look in the file COPYING for details. 
	type    dp -H    for help 
	
	Input completed --> Initializing datastructures ... 
	Initializing datastructures completed  --> Solving ... 

	 ****** INSATISFIABLE ******
	Time used (msecs) : read(16) init(0) solve(467) 
	Explored nodes : 6490     Number of unit resolutions : 23521 
	Bye ...


   Problems in the DIMACS Satisfiability format can be read in with option -0

	mpii02045 [17:07] 173 SAT -> dp -0 -h2 -t2 < cnf432.001
	dp version 0.2, Copyright (C) 1993 Peter Barth 
	dp comes with ABSOLUTELY NO WARRANTY; for details look in the file COPYING. 
	This is free software, and you are welcome to redistribute it 
	under certain conditions; look in the file COPYING for details. 
	type    dp -H    for help 

	Input completed --> Initializing datastructures ... 
	Initializing datastructures completed  --> Solving ... 

	 ****** INSATISFIABLE ******
	Time used (msecs) : read(150) init(816) solve(88950) 
	Explored nodes : 16772     Number of unit resolutions : 338126 
	Bye ...


To protect myself, see the file COPYING for copyleft.

BUGS:
	- The problem is simplified during Input.
	  Double literals and tautologies are deleted. 
	- The parser is awful, should be LEX/YACC. (You're welcome to write one)
	- maximal clause length = maximal number of clauses = 65536


Bug reports and flames are welcome (barth@mpi-sb.mpg.de).
If you have found a bug please send me the problem set as well.

Additions:
  I would be glad to receive any useful changes you've made, like
	- a good parser
	- a new super heuristic (it's fairly easy to add one)
	- remarks like "Why haven't you ..."
	               "It would be nice to ..."

Have fun
	Peter


Peter Barth
Max-Planck-Institut f. Informatik               email: barth@mpi-sb.mpg.de
Im Stadtwald                                    fax:   +49 681 302 5401
6600 Saarbr"ucken, Germany

