Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the trivialib.bdd Reference Manual, version 0.1, generated automatically by Declt version 4.0 beta 2 "William Riker" on Mon Aug 15 06:05:03 2022 GMT+0.
Next: Systems, Previous: The trivialib.bdd Reference Manual, Up: The trivialib.bdd Reference Manual [Contents][Index]
* Trivialib.Bdd
Functional implementation of (Ordered) Binary Decision Diagram (BDD) and Zero-suppressed Binary Decision Diagram (ZDD).
+ Bryant, Randal E. "Graph-based algorithms for boolean function
manipulation." Computers, IEEE Transactions on 100.8 (1986): 677-691.
+ Minato, Shin-ichi. "Zero-suppressed BDDs for set manipulation in
combinatorial problems." Design Automation, 1993. 30th Conference
on. IEEE, 1993.
[[http://users.cecs.anu.edu.au/~ssanner/AAAI16/][Tutorial slide]] on Symbolic Methods for Hybrid Inference, Optimization, and Decision-making at AAAI 2016, by [[http://users.cecs.anu.edu.au/~ssanner/][Scott Sanner]]
* FEATURES
Based on structures --- moderately fast
Weak hash table --- GC-aware, moderate memory usage
Pattern matching --- functional, clean implementation
* TODOs
+ more useful interfaces for set manipulation, function manipulation
+ speed
+ extension to ADD (Algebraic Decision Diagram) --- mostly trivial
+ extension to XADD (algebraic decision diagram)
+ extension to MV-DDs (multi-valued decision diagram)
+ extension to AADDs (affine algebrainc decision diagram) --- for representing formula
+ extension to XADDs (continuous variable extension of algebrainc decision diagram) --- for continuous range
+ extension to SDD (sentensial decision diagram)
* Usage
Web API Documentation will be available at http://quickdocs.org/trivialib.bdd/
#+BEGIN_SRC lisp
;; Knuth Chapter 4, figure 12 (and 122), rightmost ("kernel")
;; represent a set {{1,3,5},{1,4},{2,4,6},{2,5},{3,6}}
(labels ((add2 (dd1 dd2) (odd-apply dd1 dd2 (lambda (a b) (or a b))))
(mul2 (dd1 dd2) (odd-apply dd1 dd2 (lambda (a b) (and a b))))
(add (dd1 dd2 &rest args)
(if args
(apply #'add (add2 dd1 dd2) args)
(add2 dd1 dd2)))
(mul (dd1 dd2 &rest args)
(if args
(apply #'mul (mul2 dd1 dd2) args)
(mul2 dd1 dd2)))
(o (x) (odd (unit x)))
(x (x) (odd (!unit x)))
(change-many (node &rest args) (reduce #'change args :initial-value node)))
(with-odd-context (:variable '(a b c d e f))
;; stored into VARIABLES slot of an ODD. ^^^
;; Different variable orderings make ODDs incompatible.
(gcprint
;; using BDD reduction rule: 15 nodes
(add (mul (o 1) (x 2) (o 3) (x 4) (o 5) (x 6))
(mul (o 1) (x 2) (x 3) (o 4) (x 5) (x 6))
(mul (x 1) (o 2) (x 3) (o 4) (x 5) (o 6))
(mul (x 1) (o 2) (x 3) (x 4) (o 5) (x 6))
(mul (x 1) (x 2) (o 3) (x 4) (x 5) (o 6)))))
(with-odd-context (:operation #'zdd-apply)
;; Different reduction rule also make ODDs incompatible.
(gcprint
;; using Zero-suppressed reduction rule: 8 nodes
(add (odd (change-many (leaf t) 1 3 5))
(odd (change-many (leaf t) 1 4))
(odd (change-many (leaf t) 2 4 6))
(odd (change-many (leaf t) 2 5))
(odd (change-many (leaf t) 3 6)))))
(with-odd-context (:operation #'zdd-apply)
;; using a utility function for ZDD
(gcprint
(add (odd (make-set '(1 3 5)))
(odd (make-set '(1 4)))
(odd (make-set '(2 4 6)))
(odd (make-set '(2 5)))
(odd (make-set '(3 6))))))
(with-odd-context (:operation #'zdd-apply)
;; using a utility function for ZDD
(gcprint
(odd (make-family '((1 3 5)
(1 4)
(2 4 6)
(2 5)
(3 6)))))))
#+END_SRC
** Dependencies
This library is at least tested on implementation listed below:
+ SBCL 1.2.8 on X86-64 Linux 3.13.0-46-generic (author's environment)
Also, it depends on the following libraries:
+ alexandria by ::
Alexandria is a collection of portable public domain utilities.
+ trivia by Masataro Asai ::
NON-optimized pattern matcher compatible with OPTIMA, with extensible optimizer interface and clean codebase
+ immutabe-struct by Masataro Asai ::
+ trivial-garbage :: For handling weak hash tables.
** Author
+ Masataro Asai (guicho2.71828@gmail.com)
* Copyright
Copyright (c) 2015 Masataro Asai (guicho2.71828@gmail.com)
* License
Licensed under the LLGPL License.
Next: Files, Previous: Introduction, Up: The trivialib.bdd Reference Manual [Contents][Index]
The main system appears first, followed by any subsystem dependency.
BDD and ZDD implementation using Trivia
Masataro Asai
LLGPL
0.1
Next: Packages, Previous: Systems, Up: The trivialib.bdd Reference Manual [Contents][Index]
Files are sorted by type and then listed depth-first from the systems components trees.
Next: trivialib.bdd/0.package.lisp, Previous: Lisp, Up: Lisp [Contents][Index]
trivialib.bdd (system).
Next: trivialib.bdd/1.struct.lisp, Previous: trivialib.bdd/trivialib.bdd.asd, Up: Lisp [Contents][Index]
trivialib.bdd (system).
Next: trivialib.bdd/2.odd.lisp, Previous: trivialib.bdd/0.package.lisp, Up: Lisp [Contents][Index]
0.package.lisp (file).
trivialib.bdd (system).
Next: trivialib.bdd/3.bdd.lisp, Previous: trivialib.bdd/1.struct.lisp, Up: Lisp [Contents][Index]
1.struct.lisp (file).
trivialib.bdd (system).
Next: trivialib.bdd/4.zdd.lisp, Previous: trivialib.bdd/2.odd.lisp, Up: Lisp [Contents][Index]
2.odd.lisp (file).
trivialib.bdd (system).
Previous: trivialib.bdd/3.bdd.lisp, Up: Lisp [Contents][Index]
3.bdd.lisp (file).
trivialib.bdd (system).
Next: Definitions, Previous: Files, Up: The trivialib.bdd Reference Manual [Contents][Index]
Packages are listed by definition order.
Next: Indexes, Previous: Packages, Up: The trivialib.bdd Reference Manual [Contents][Index]
Definitions are sorted by export status, category, package, and then by lexicographic order.
Next: Internals, Previous: Definitions, Up: Definitions [Contents][Index]
Next: Ordinary functions, Previous: Public Interface, Up: Public Interface [Contents][Index]
Execute BODY in a dynamic environment where the context variables
(‘*VARIABLES*’ , ‘*NODE-CACHE*’ and ‘*OPERATION*’) are set.
DEFAULT should be nil or an ODD object, in which case
the context variables are inherited by the given ODD.
Next: Structures, Previous: Macros, Up: Public Interface [Contents][Index]
Returns a BDD node whose HI node is a terminal node of NIL and LO node is a terminal node of T (opposite to UNIT). Useful for representing a boolean variable.
Shortcut for instantiating an ODD using BDD-APPLY.
APPLY rule for BDD.
Node generation & pruning rule for BDD.
Function version of WITH-ODD-CONTEXT.
Change operation defined in MINATO et al. 93’. Flip the existense of a given variable in the family of sets.
Examples:
(change {{1,3} {2,5}} 6) –> {{1,3,6} {2,5,6}}
(change {{1,3} {2,5,6}} 6) –> {{1,3,6} {2,5}}
Return the leaf node in the hash table *leaf-cache*, creating an instance when required
Example: (make-family ’((1 3 5) (2 4))) –> a zdd representing {{1,3,5},{2,4}}
Example: (make-set ’(1 3 5)) –> a zdd representing {{1,3,5}}
Applies the operation stored in ODD, recursively. At the leaf-level, applies LEAF-OPERATION.
Returns a BDD node whose HI node is a terminal node of T and LO node is a terminal node of NIL. Useful for representing a boolean variable.
Shortcut for instantiating an ODD using ZDD-APPLY.
APPLY rule for ZDD.
Node generation & pruning rule for ZDD.
Previous: Ordinary functions, Up: Public Interface [Contents][Index]
Leaf node of a decision diagram
structure-object.
lightweight node in Decision Diagram.
VARIABLE: an integer representing the index of a variable. cf. VARIABLES slot in structure DD
HI,LO: hi/lo pointer
structure-object.
common-lisp.
fixnum
0
(or trivialib.bdd:node trivialib.bdd:leaf)
(trivialib.bdd:leaf nil)
(or trivialib.bdd:node trivialib.bdd:leaf)
(trivialib.bdd:leaf nil)
Structure representing a whole Decision Diagram.
Holds the context information such as variables and node-cache.
For different variable ordering, ODDs are incompatible.
structure-object.
none (uninterned).
(or trivialib.bdd:node trivialib.bdd:leaf)
(trivialib.bdd:leaf nil)
This slot is read-only.
none (uninterned).
sequence
trivialib.bdd::*variables*
This slot is read-only.
none (uninterned).
hash-table
trivialib.bdd::*node-cache*
This slot is read-only.
none (uninterned).
(function ((or trivialib.bdd:node trivialib.bdd:leaf) (or trivialib.bdd:node trivialib.bdd:leaf) (function (t t) *)) (or trivialib.bdd:node trivialib.bdd:leaf))
trivialib.bdd::*operation*
This slot is read-only.
Previous: Public Interface, Up: Definitions [Contents][Index]
Next: Ordinary functions, Previous: Internals, Up: Internals [Contents][Index]
hash table to look up a leaf node of a thing.
Hash table to look up in order to avoid the creation of redundunt nodes.
This cache is specific to the ODD context defined by the pair of variables and operation(BDD-APPLY or ZDD-APPLY).
Generic operations for a decision diagram in the current context, either #’BDD-APPLY or #’ZDD-APPLY.
ODD variables in the current context.
Previous: Special variables, Up: Internals [Contents][Index]
Check if two ODDs have the same variable ordering, node-cache, and operations.
Previous: Definitions, Up: The trivialib.bdd Reference Manual [Contents][Index]
| Jump to: | !
(
B C F L M N O U W Z |
|---|
| Jump to: | !
(
B C F L M N O U W Z |
|---|
Next: Data types, Previous: Functions, Up: Indexes [Contents][Index]
| Jump to: | *
C H L N O R S V |
|---|
| Jump to: | *
C H L N O R S V |
|---|
| Jump to: | 0
1
2
3
4
F L N O P S T |
|---|
| Jump to: | 0
1
2
3
4
F L N O P S T |
|---|