Author: Scott Sanner
Email:  ssanner @ cs . toronto . edu

Quick notes on the RCBDD software:

1) This code requires a number of libraries, most importantly the
   CUDD library.  I've provided the binaries for a Linux/Intel
   system.  **If your system is different**, you'll have to obtain CUDD
   from Fabio Somenzi's home page,

     http://vlsi.colorado.edu/~fabio/

   and compile the libraries yourself.  Place the libraries (i.e., 
   the '.a' files) in the 'cudd' subdirectory of this project.

   Documentation for CUDD can be found at:

     http://vlsi.colorado.edu/~fabio/CUDD/

   I've used the GNU g++ compiler for all of my builds.

2) To compile the RCBDD code on a UNIX system, just type 'make'.

3) To run the SAT engine, use the following command line syntax:

     rcbdd [bdd|rc] <SAT Problem File>

     'bdd' indicates to use standard bdd inference.
     'rc'  indicates to use refutation-complete bdd inference.

4) There are two test cnf files in the main project directory... 

     'tests.cnf' - A satisfiable set of cnf formulae.
     'testu.cnf' - An unsatisfiable set of cnf formulae.

   Following are four possible command lines and the result of inference:

     'rcbdd bdd tests.cnf' - Run the bdd algorithm on 'tests.cnf' -> SAT
     'rcbdd bdd testu.cnf' - Run the bdd algorithm on 'testu.cnf' -> UNSAT
     'rcbdd rc  tests.cnf' - Run the rc algorithm on 'tests.cnf' -> SAT
     'rcbdd rc  testu.cnf' - Run the rc algorithm on 'testu.cnf' -> UNSAT

   For an overview of the '.cnf' file format, check out:

     http://www.satlib.org/Benchmarks/SAT/satformat.ps

   A huge library of sample cnf files can be found at:

     http://www.satlib.org/

6) The performance characteristics of the standard 'bdd' and refutation-
   complete 'rc' algorithms differ based on the problem type.  For details,
   check out the paper 'Refutation-Complete Binary Decision Diagrams': 

     http://www.cs.toronto.edu/~ssanner/Papers/rcbdd.ps.gz
     http://www.cs.toronto.edu/~ssanner/Papers/rcbdd.pdf