Software Library Extending CUDD Package (rel 2.3.1)
- The library is to be used with the decision diagram package, CUDD
- New ZBDD operations are introduced that can be called from any application
source code just like any normal CUDD procedure.
- Library is mainly to be used to manipulate CNF formulas.
- Some procedures are specifically defined to be used with Satometer.
- All procedures should run fine with dynamic variable reordering.
- In case of any errors, please report them to email@example.com
- Complete Library, version 0.1
- Individual files, version 0.1
Cudd_zddCountLitDouble: Counts the number of
literals in a ZBDD respresenting a set of clauses
Cudd_zddCountSpace: Counts the explored search
space eliminated by a set of clauses (used with Satometer)
Cudd_zddNoSub*: Eliminates subsumed clauses
Cudd_zddNoSubA**: Eliminates subsumed clauses
and tautologies and performs a combination of Boolean Algebraic manipulations
(i.e. absorbtion, subsumption, and resolution).
Cudd_zddUnionS*: Unions (ANDs) clauses with
subsumption check enabled
Cudd_zddUnionSA**: Unions (ANDs) clauses with
subsumption check + algebraic manipulation techniques enabled
Cudd_zddUnionReg: Unions (ANDs) clauses without
* proposed in [Chatalic and Simon, ICTAI'00]
** proposed in [Aloul et al., IWLS'01]
Installation (3 parts)
- A) Installing CUDD
- Download and install the CUDD package.
- B) Installing Zbdd library
- Save ZbddCuddLib in the CUDD directory.
- Create a directory "lib" in the CUDD directory.
- Untar the ZbddCudd library.
- Run make in the zbddLib directory.
- C) Linking your application with the Zbdd library
- Include in your application a path to the "zbddLib/zlib.h"
- Add the "zLib.a" to the application makefile. You will need
to specify the location of the library "cudd-2.3.1/lib".
- Compile your application.
Maintained by Fadi Aloul (firstname.lastname@example.org)
Last updated Mon June 17, 2002