Skip to content

A simple Python Binary Decision Diagram (BDD) that outputs .dot files. It can also create minimal BDDs. Should be used mostly for educational purposes as it is not very efficient. Try it out online here: http://formal.cs.utah.edu:8080/pbl/BDD.php

License

Notifications You must be signed in to change notification settings

tyler-utah/PBDD

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 

Repository files navigation

A BDD package written in Python largly based off of 
Anderson's notes found:
http://configit.com/configit_wordpress/wp-content/uploads/2013/07/bdd-eap.pdf

This software is released under a BSD lisense, so feel free to do whatever
you'd like with it. Please drop me an email though if you find it
useful or have any questions or comments:
t.sorensen@utah.edu

Requires:

PBL : a python boolean algebra library (also developed and maintained
by Tyler Sorensen)

PLY : python bindings to yacc and lex (needed by PBL).

Complete examples on how to run are found in the examples directory
Please see PBL docs for a language description.

All public interface functions should be documented in include/BDD.py
but are reproduced here:

def bdd_init(fName):
    """
    Initializes a BDD data structure (dictionary) with the 
    Boolean Formula stored in file name FNAME.
    """


def build(bdd):
    """
    Public function to build the BDD. See ite_build
    for a more efficient build
    """

def any_sat(bdd):

    """
    Public function to any_sat. Simply returns an arbitrary
    satisfying assignement as a list, or [] if none.  
    """

def sat_count(bdd):
    """
    Public function sat_count, returns the number of satisfying
    assignments
    """

def all_sat(bdd):
    """
    Public function all_sat. Returns all satisfiying assignments
    in a list of lists form
    """

def dot_bdd(bdd, fname):
    """
    prints a dot file FNAME representing the binary decision
    diagram BDD
    """

def stat_string(bdd):
    """
    Return a string with some stats about the BDD
    """

def ite_build(bdd):
    """
    Implementation of the efficient 'ite' method of building a BDD
    discussed in Bryan et al's paper "Efficient Implementation of a
    BDD Package" Often more efficient than regular build.    
    """

Tyler Sorensen

About

A simple Python Binary Decision Diagram (BDD) that outputs .dot files. It can also create minimal BDDs. Should be used mostly for educational purposes as it is not very efficient. Try it out online here: http://formal.cs.utah.edu:8080/pbl/BDD.php

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages