ZBDD Library

Introduction

• The library is to be used with the decision diagram package, CUDD Release 2.3.1.
• 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 faloul@aus.edu
  

Download

• Complete Library, version 0.1
  
  • Source code - [zbddCuddLib_v01.tar.gz]
    
    
• Individual files, version 0.1
• Makefile
• zCountLit.c
  Cudd_zddCountLitDouble: Counts the number of literals in a ZBDD respresenting a set of clauses
• zCountSpace.c
  Cudd_zddCountSpace: Counts the explored search space eliminated by a set of clauses (used with Satometer)
• zSubsume.c
  Cudd_zddNoSub*: Eliminates subsumed clauses and tautologies
  Cudd_zddNoSubA**: Eliminates subsumed clauses and tautologies and performs a combination of Boolean Algebraic manipulations (i.e. absorbtion, subsumption, and resolution).
• zUnionS.c
  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 subsumption check
  
  

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

* proposed in [Chatalic and Simon, ICTAI'00]
** proposed in [Aloul et al., IWLS'01]

Installation (3 parts)

• A) Installing CUDD
  1. Download and install the CUDD package.
     
     
• B) Installing Zbdd library
  1. Save ZbddCuddLib in the CUDD directory.
  2. Create a directory "lib" in the CUDD directory.
  3. Untar the ZbddCudd library.
  4. Run make in the zbddLib directory.
     
     
• C) Linking your application with the Zbdd library
  1. Include in your application a path to the "zbddLib/zlib.h" header file.
  2. Add the "zLib.a" to the application makefile. You will need to specify the location of the library "cudd-2.3.1/lib".
  3. Compile your application.

Enjoy!