An Introduction to Binary Decision Diagrams [pdf] | Hacker News Reader

An Introduction to Binary Decision Diagrams [pdf]

cs.utexas.edu

101 pointsmindcrime26 comments

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.

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.

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

Slides for the book are here, https://web.stanford.edu/class/cs156/slides/Technion/

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"...)

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.

Ben Lynn's "Award winning compiler" is one of my favorites, and he keeps adding to that page.

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 .

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

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...

> 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.

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

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?

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

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.

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

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.

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).

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.

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/).

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.

Aren't BDDs used extensively in hardware synthesis?

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).

> #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

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

or directed graph

BDDs are used heavily in logic synthesis for hardware.

Reply on news.ycombinator.com