Implementation of the Binary Decision Diagrams in Racket
This is experimental library which implements Binary Decision Diagrams
(BDD) in Racket programming language.
This is not production library. It will be changed without preserving
backward compatibility in the future. Library implements Reduced
Ordered Binary Decision Diagrams (ROBDD) and Zero-Suppressed
Binary Decision Diagrams (ZDD). My intent is to add implementation of
functions transforming ROBDD into ZDD and vice versa. I was inspired
by papers [1], [2].
This code is released under MIT License.
Copyright (c) 2016 Peter Cerman (https://github.com/pcerman)
ROBDD
(require "bdd.rkt" "robdd.rkt")(define ex '(xor (xor x y) z));; create ROBDD for this boolean expression(define bdd (make-robdd ex '(x y z)));; create graph representation of this ROBDD and write it into the file(bdd->tgf bdd "bdd.tgf" '(x y z));; count number of solutions which evaluates to boolean value true(robdd-sat-count bdd 3);; it returns: 4;; transform ROBDD into boolean expression(robdd->b-expr bdd '(x y z));; it returns: '(or (and x (or (and y z) (and (not y) (not z))));; (and (not x) (or (and y (not z)) (and (not y) z))))
Graph representation of the ROBDD from example:
ZDD
(require "bdd.rkt" "zdd.rkt")(define ex '(xor (xor x y) z));; create ZDD for this boolean expression(define zdd (make-zdd ex '(x y z)));; create graph representation of this ZDD and write it into the file(bdd->tgf zdd "zdd.tgf" '(x y z));; count number of solutions which evaluates to boolean value true(zdd-count zdd);; it returns: 4;; transform ZDD into boolean expression(zdd->b-expr zdd '(x y z));; it returns: '(or (and x (or (and y z) (and (not y) (not z))));; (and (not x) (or (and y (not z)) (and (not y) z))))
Graph representation of the ZDD from example. It represents subset
{ {x}, {y}, {z}, {x,y,z} } of powerset from {x,y,z}.