4 ms·

An Introduction to Binary Decision Diagrams [pdf]

101 points by mindcrime 4y ago

fcholf 4y ago
Interesting to see it posted on HN. My favourite book on the subject is Branching Programs and Binary Decision Diagrams by Ingo Wegener: https://doi.org/10.1137/1.9780898719789 https://doi.org/10.1137/1.9780898719789. There have been recent exciting developments of the same underlying idea for more complicated data structures (consisting in syntactic restrictions of Boolean circuits) with applications to other domains in computer science. This is known as "knowledge compilation" where the original goal is to transform a knowledge base offline to represent it to a more tractable data structure efficiently supporting "online" queries such as model counting and conditioning. See for example some of the knowledge compilers listed here http://beyondnp.org/pages/solvers/knowledge-compilers/ http://beyondnp.org/pages/solvers/knowledge-compilers/ for Boolean functions, applications to databases with so called factorized databases https://fdbresearch.github.io/index.html https://fdbresearch.github.io/index.html.
- dragontamer 4y ago
  The main issue with that book is that it talks about BDDs in general, as opposed to the most common ROBDD that people are probably interested in. Its a lot of 'spinning up' to start from branching programs and working your way to ROBDDs. In many ways, ROBDDs are easier than a lot of the stuff discussed earlier in the book. So the layout probably should be reworked. But otherwise, the info is all there, and its good that the book hits "rock bottom" so to speak, with regards to theory.
  - sitkack 4y ago
    What do you both think of "The Calculus of Computation" by Bradley and Manna? https://link.springer.com/book/10.1007/978-3-540-74113-8 https://link.springer.com/book/10.1007/978-3-540-74113-8 Slides for the book are here, https://web.stanford.edu/class/cs156/slides/Technion/ https://web.stanford.edu/class/cs156/slides/Technion/
tromp 4y ago
One impressive application of these is counting state spaces. In [1], Stefan Edelkamp and Peter Kissmann count the number of connect-4 positions: > Symbolic search is concerned with checking the satisfiability of formulas. For this purpose, we use Binary Decision Diagrams (BDDs), so that we work with state sets instead of single states. In many cases, this saves a lot of memory. E. g., we are able to calculate the complete set of reachable states for Connect Four. The precise number of states reachable from the initially empty board is 4,531,985,219,092, compared to Allis’s estimate of 70,728,639,995,483. In case of explicit search, for the same state encoding (two bits for each cell (player 1, player 2, empty) plus one for the current player, resulting in a total of 85 bits per state), nearly 43.8 terabytes would be necessary. When using BDDs, 84,088,763 nodes suffice to represent all states. I discovered their paper after doing a brute-force count myself (although clever partitioning allowed me to get away with only a dozen GB of memory), and googling the final count (expecting 0 hits) [2]. [1] https://fai.cs.uni-saarland.de/kissmann/publications/ki08-ggpsolver.pdf https://fai.cs.uni-saarland.de/kissmann/publications/ki08-gg... [2] https://tromp.github.io/c4/c4.html https://tromp.github.io/c4/c4.html
- vjerancrnjak 4y ago
  Zero suppressed decision diagrams work even better (less nodes). I think TAoCP Vol. 4 goes through a bunch of examples that applies them and has interesting counting problems whose instances are solved for large N. Every now and then I think a bit on how to apply this to something more serious (problems with constraints) but still haven't found an approach. 0: https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagram https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagr...
  - dragontamer 4y ago
    > Zero suppressed decision diagrams work even better (less nodes) No. Zero suppressed decision diagrams (aka: ZDDs) *sometimes* work better than ROBDDs (the default). Its difficult to know which style of decision diagram is best for any application. There's lots of different pros-and-cons, and different styles. But the majority of Knuth's TAoCP Volume4 is on ROBDDs (or BDDs for short) for a reason, they're one of the "original" and broadly applicable. ----------- I'd say that BDDs / ROBDDs work best with so called "symmetric" functions. XOR, AND, OR, Addition... these are all "symmetric" (based off of the _count_ of its input bits, rather than an arbitrary function), and therefore very efficient to represent in BDDs. Functions built up "out of" symmetric functions are also reasonably efficient. So multiplication is built up from a lot of additions. So its not as efficient as addition, but efficient enough that we can represent 128-bit inputs and 128-bit outputs (ie: 64-bit x 64-bit == 128-bit output) kinds of functions with BDDs.
suyjuris 4y ago
If you want to explore how BDD algorithms work visually, with animations, I did write an open-source tool for exactly this purpose a while ago: https://nicze.de/philipp/bdds/ https://nicze.de/philipp/bdds/ Let me know if it is of any use! :) Sources are at https://github.com/suyjuris/obst https://github.com/suyjuris/obst .
freemint 4y ago
I've always wondered how those can be performant at all compared to approaches like SAT.
- fcholf 4y ago
  This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying assignment using a vanilla SAT-solver would be quite bad as you would end up generating every assignment while OBDD can sometimes take advantage of factorizing some part of the input. But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.
  - freemint 4y ago
    There are also sat solvers which do (approximate) solution counting. It is just that all these pointers seems so cache unfriendly ... But thank you for your insight
    - dragontamer 4y ago
      See the paper "The Number of Knight's Tours Equals 33,439,123,484,294 | Counting with Binary Decision Diagrams" by Martin Lobbing and Ingo Wegener. Bonus points, this occurred in the 80s, when computers only had kilobytes of memory (not even MBs). So... yeah, BDDs are an incredibly powerful technique. BDDs obtain an exact count, and are among the most efficient algorithms for this problem. "Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.
carapace 4y ago
Knuth - "Fun With Binary Decision Diagrams (BDDs)" (June 5, 2008) https://www.youtube.com/watch?v=SQE21efsf7Y https://www.youtube.com/watch?v=SQE21efsf7Y He has some other good material on BDDs, some of it in TAoCP. (My search fu is failing me this morning. I found https://crypto.stanford.edu/pbc/notes/zdd/ https://crypto.stanford.edu/pbc/notes/zdd/ which seems interesting, and Ben Lynn has some cool stuff linked from his home page: "Lambda calculus one-line self-interpreter", "Haskell compiler that runs in the browser"...)
- dubya 4y ago
  Knuth also has sample code here: https://www-cs-faculty.stanford.edu/~knuth/programs.html https://www-cs-faculty.stanford.edu/~knuth/programs.html I couldn't get some of it to work due to pointer hijinks not cooperating with Macos, but it's fine in a Linux vm.
- dunham 4y ago
  Ben Lynn's "Award winning compiler" is one of my favorites, and he keeps adding to that page.
UncleOxidant 4y ago
BDDs are used heavily in logic synthesis for hardware.
kherud 4y ago
Without being particularly familiar with it, I wonder how BDDs differ from the generalization to multivalued decision diagrams (MDDs)? For example, in constraint satisfaction problems, variables often have more than two values. However, in the context of decision diagrams, you rarely hear about MDDs. Are there theoretical advantages of the binary restriction?
koheripbal 4y ago
Does know what the optimal database schema to store these diagrams would be?
- mistrial9 4y ago
  or directed graph

101 points by mindcrime 4y ago

Interesting to see it posted on HN. My favourite book on the subject is Branching Programs and Binary Decision Diagrams by Ingo Wegener: https://doi.org/10.1137/1.9780898719789 https://doi.org/10.1137/1.9780898719789. There have been recent exciting developments of the same underlying idea for more complicated data structures (consisting in syntactic restrictions of Boolean circuits) with applications to other domains in computer science. This is known as "knowledge compilation" where the original goal is to transform a knowledge base offline to represent it to a more tractable data structure efficiently supporting "online" queries such as model counting and conditioning. See for example some of the knowledge compilers listed here http://beyondnp.org/pages/solvers/knowledge-compilers/ http://beyondnp.org/pages/solvers/knowledge-compilers/ for Boolean functions, applications to databases with so called factorized databases https://fdbresearch.github.io/index.html https://fdbresearch.github.io/index.html.

dragontamer 4y ago
The main issue with that book is that it talks about BDDs in general, as opposed to the most common ROBDD that people are probably interested in. Its a lot of 'spinning up' to start from branching programs and working your way to ROBDDs. In many ways, ROBDDs are easier than a lot of the stuff discussed earlier in the book. So the layout probably should be reworked. But otherwise, the info is all there, and its good that the book hits "rock bottom" so to speak, with regards to theory.
- sitkack 4y ago
  What do you both think of "The Calculus of Computation" by Bradley and Manna? https://link.springer.com/book/10.1007/978-3-540-74113-8 https://link.springer.com/book/10.1007/978-3-540-74113-8 Slides for the book are here, https://web.stanford.edu/class/cs156/slides/Technion/ https://web.stanford.edu/class/cs156/slides/Technion/

tromp 4y ago

One impressive application of these is counting state spaces. In [1], Stefan Edelkamp and Peter Kissmann count the number of connect-4 positions: > Symbolic search is concerned with checking the satisfiability of formulas. For this purpose, we use Binary Decision Diagrams (BDDs), so that we work with state sets instead of single states. In many cases, this saves a lot of memory. E. g., we are able to calculate the complete set of reachable states for Connect Four. The precise number of states reachable from the initially empty board is 4,531,985,219,092, compared to Allis’s estimate of 70,728,639,995,483. In case of explicit search, for the same state encoding (two bits for each cell (player 1, player 2, empty) plus one for the current player, resulting in a total of 85 bits per state), nearly 43.8 terabytes would be necessary. When using BDDs, 84,088,763 nodes suffice to represent all states. I discovered their paper after doing a brute-force count myself (although clever partitioning allowed me to get away with only a dozen GB of memory), and googling the final count (expecting 0 hits) [2]. [1] https://fai.cs.uni-saarland.de/kissmann/publications/ki08-ggpsolver.pdf https://fai.cs.uni-saarland.de/kissmann/publications/ki08-gg... [2] https://tromp.github.io/c4/c4.html https://tromp.github.io/c4/c4.html

vjerancrnjak 4y ago
Zero suppressed decision diagrams work even better (less nodes). I think TAoCP Vol. 4 goes through a bunch of examples that applies them and has interesting counting problems whose instances are solved for large N. Every now and then I think a bit on how to apply this to something more serious (problems with constraints) but still haven't found an approach. 0: https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagram https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagr...
- dragontamer 4y ago
  > Zero suppressed decision diagrams work even better (less nodes) No. Zero suppressed decision diagrams (aka: ZDDs) *sometimes* work better than ROBDDs (the default). Its difficult to know which style of decision diagram is best for any application. There's lots of different pros-and-cons, and different styles. But the majority of Knuth's TAoCP Volume4 is on ROBDDs (or BDDs for short) for a reason, they're one of the "original" and broadly applicable. ----------- I'd say that BDDs / ROBDDs work best with so called "symmetric" functions. XOR, AND, OR, Addition... these are all "symmetric" (based off of the _count_ of its input bits, rather than an arbitrary function), and therefore very efficient to represent in BDDs. Functions built up "out of" symmetric functions are also reasonably efficient. So multiplication is built up from a lot of additions. So its not as efficient as addition, but efficient enough that we can represent 128-bit inputs and 128-bit outputs (ie: 64-bit x 64-bit == 128-bit output) kinds of functions with BDDs.

suyjuris 4y ago

If you want to explore how BDD algorithms work visually, with animations, I did write an open-source tool for exactly this purpose a while ago: https://nicze.de/philipp/bdds/ https://nicze.de/philipp/bdds/ Let me know if it is of any use! :) Sources are at https://github.com/suyjuris/obst https://github.com/suyjuris/obst .

freemint 4y ago

I've always wondered how those can be performant at all compared to approaches like SAT.

fcholf 4y ago
This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying assignment using a vanilla SAT-solver would be quite bad as you would end up generating every assignment while OBDD can sometimes take advantage of factorizing some part of the input. But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.
- freemint 4y ago
  There are also sat solvers which do (approximate) solution counting. It is just that all these pointers seems so cache unfriendly ... But thank you for your insight
  - dragontamer 4y ago
    See the paper "The Number of Knight's Tours Equals 33,439,123,484,294 | Counting with Binary Decision Diagrams" by Martin Lobbing and Ingo Wegener. Bonus points, this occurred in the 80s, when computers only had kilobytes of memory (not even MBs). So... yeah, BDDs are an incredibly powerful technique. BDDs obtain an exact count, and are among the most efficient algorithms for this problem. "Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.

carapace 4y ago

Knuth - "Fun With Binary Decision Diagrams (BDDs)" (June 5, 2008) https://www.youtube.com/watch?v=SQE21efsf7Y https://www.youtube.com/watch?v=SQE21efsf7Y He has some other good material on BDDs, some of it in TAoCP. (My search fu is failing me this morning. I found https://crypto.stanford.edu/pbc/notes/zdd/ https://crypto.stanford.edu/pbc/notes/zdd/ which seems interesting, and Ben Lynn has some cool stuff linked from his home page: "Lambda calculus one-line self-interpreter", "Haskell compiler that runs in the browser"...)

dubya 4y ago
Knuth also has sample code here: https://www-cs-faculty.stanford.edu/~knuth/programs.html https://www-cs-faculty.stanford.edu/~knuth/programs.html I couldn't get some of it to work due to pointer hijinks not cooperating with Macos, but it's fine in a Linux vm.
dunham 4y ago
Ben Lynn's "Award winning compiler" is one of my favorites, and he keeps adding to that page.

UncleOxidant 4y ago

BDDs are used heavily in logic synthesis for hardware.

kherud 4y ago

Without being particularly familiar with it, I wonder how BDDs differ from the generalization to multivalued decision diagrams (MDDs)? For example, in constraint satisfaction problems, variables often have more than two values. However, in the context of decision diagrams, you rarely hear about MDDs. Are there theoretical advantages of the binary restriction?

koheripbal 4y ago

Does know what the optimal database schema to store these diagrams would be?

mistrial9 4y ago
or directed graph