[HN Gopher] An Introduction to Binary Decision Diagrams [pdf]
___________________________________________________________________
An Introduction to Binary Decision Diagrams [pdf]
Author : mindcrime
Score : 95 points
Date : 2022-09-27 08:59 UTC (14 hours ago)
(HTM) web link (www.cs.utexas.edu)
(TXT) w3m dump (www.cs.utexas.edu)
| koheripbal wrote:
| Does know what the optimal database schema to store these
| diagrams would be?
| mistrial9 wrote:
| or directed graph
| UncleOxidant wrote:
| BDDs are used heavily in logic synthesis for hardware.
| fcholf wrote:
| 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.
|
| 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/ for
| Boolean functions, applications to databases with so called
| factorized databases https://fdbresearch.github.io/index.html.
| dragontamer wrote:
| 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.
| tromp wrote:
| 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-gg...
|
| [2] https://tromp.github.io/c4/c4.html
| vjerancrnjak wrote:
| 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_diagr...
| dragontamer wrote:
| > 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.
| boothby wrote:
| Obligatory plug for Sloane's encyclopedia of integer sequences!
| Every time I embark on a combinatorial investigation, I collect
| some statistics and search Sloane's. It's rare that I don't get
| useful hits.
|
| https://oeis.org/search?q=1104642469
| freemint wrote:
| I've always wondered how those can be performant at all compared
| to approaches like SAT.
| fcholf wrote:
| 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 wrote:
| 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
| fcholf wrote:
| I would be curious to know examples of SAT solvers you have
| in mind for approximate counting. The only tools I am aware
| of for approximate counting are dedicated to this task (and
| usually use SAT solvers as oracles under the hood).
| dragontamer wrote:
| 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.
| comfypotato wrote:
| Second paragraph of 382 of
| http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf mentions how
| SAT solvers create BDD. I'm not super familiar with using the
| proofs of unsat from a solver, but I think it's basically the
| BDD that shows there is no satisfying assignment.
| fcholf wrote:
| Well this is true but CDCL SAT solvers do not materialize
| this BDD and they stop as soon as they find a satisfying
| assignment. If they do not find any satisfying assignment,
| they do not return the BDD as unsat proof but roughly the
| list of learnt clause. If these clauses have been learnt
| using vanilla CDCL solver technique, one can check from this
| that the formula is indeed unsat. See the (D)RAT proof format
| (check e.g., references listed for this tool
| https://www.cs.utexas.edu/~marijn/drat-trim/).
| UncleMeat wrote:
| BDDs have been widely used in static analysis. They can be
| incredibly powerful but have an enormous weakness - their
| exponential reduction in size depends in large part on the term
| ordering and computing optimal term orderings is NP-Complete.
| Various systems have been developed to use ML to propose
| effective term orderings but my experience has been that
| performance is so finicky that you cannot actually rely on
| tools like BDDBDDB to back up industrial systems because of
| this.
| dragontamer wrote:
| SAT is for NP complete problems.
|
| BDD is for #P complete problems. IE: counting the number of
| solutions to an NP complete problem, like circuit analysis
| where having the total count of 1 output vs 0 output is useful.
|
| #P complete is at least as difficult as NP complete.
|
| --------
|
| BDDs seem like they can be used with the easier NP complete
| space, especially for optimization problems. But it's a bit
| indirect, as BDDs kinda represent an entire search space rather
| than just one solution.
|
| BDDs are useful in optimization, where having a dynamically
| updated efficient tree of all possible solutions (as currently
| understood by the algorithm), or at least an estimate of the
| search space, is useful.
|
| I read a cool paper on restricted BDDs and relaxed BDDs, where
| one BDD overestimates all 'true' solutions, and the other
| underestimates all 'true'. Since they are estimates, they are
| bounded in space (and therefore bounded in time to process).
| The relaxed+restricted BDDs serve as search guides to some
| optimization problem in NP with reasonable efficiency.
|
| Giving a better guide than previous guides (ie: arc consistency
| or path consistency have very little flexibility with regards
| to space taken up / time spent on the heuristic. But
| relaxed+restricted BDDs can achieve a similar guided heuristic
| effect with better controls over size and time).
| fcholf wrote:
| > #P complete is at least as difficult as NP complete.
|
| This is an euphemism :)! It is quite likely that #P is way
| harder than NP as witnessed by Toda's Theorem
| https://en.wikipedia.org/wiki/Toda%27s_theorem
| suyjuris wrote:
| 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/
|
| Let me know if it is of any use! :)
|
| Sources are at https://github.com/suyjuris/obst .
| carapace wrote:
| Knuth - "Fun With Binary Decision Diagrams (BDDs)" (June 5, 2008)
|
| 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/ 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"...)
| dunham wrote:
| Ben Lynn's "Award winning compiler" is one of my favorites, and
| he keeps adding to that page.
| dubya wrote:
| Knuth also has sample code here:
|
| 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.
| kherud wrote:
| 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?
___________________________________________________________________
(page generated 2022-09-27 23:02 UTC)