
dp.tar.Z

This package contains the ANSI C sources of an implementation of the
well known Davis Puttnam 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).
A Problem description ends with 'ENDATA' or <EOF>.
Characters are ignored while scanning the input.


REMARKS:
  No monotone variable fixing is done.
  Up to now 3 variable choosing heuristics:
	  none           (first occurrence, default)
	  Jeroslow/Wang  (as described in their paper
	                "Solving prop. sat. problems")
	  max. number of occurrences

  The implementation uses some index-datastructure. The memory requirements seem
  to be relatively small. 

type dp -H for a short help

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

3) Test it. (for example)
	mpii02000 [13:43] 661 X -> dp -t2 < hole6
	dp version 0.1, 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 some help 

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

	 ****** INSATISFIABLE ******
	Time used (msecs) : read(40) init(10) solve(530) 

	Bye ...



To protect myself, see the file COPYING for copyleft.

BUGS:
	- The parser is awful, should be LEX/YACC. (You're welcome to write one)
	- maximal clause length = maximal number of clauses = 65536
	- The heuristics should be faster
	- If the problem is satisfiable, no assignment is shown

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:
  If 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


