Binary Decision Diagrams (2010)
crypto.stanford.edu
crypto.stanford.edu
I mean, are there like 2 or 3 pages missing?
The real question is why was this particular link submitted as newsworthy and why did it get to the front page of HN? It is just a sidebar on the thing the author was actually writing about.
It's not just you. This article is written in the "terse yet barely comprehensible" fashion of someone wanting to cut to the chase, but leaving out so many details that the point or flow of it goes missing for anyone not in the author's head.
Lots of interesting stuff on that web site though. (There are a handful of other article series too.)
Other times though... I wonder.
And some shameless promotion, I maintain Haskell bindings for a BDD library: https://github.com/m4lvin/HasCacBDD
For a recent and comprehensive coverage, you can check out D. Knuth's fascicle as part of his well-known book. The BDD fascicle and other fascicles are available at http://www.cs.utsa.edu/~wagner/knuth/ .
My current employer, nextmv (YC W20), has built our solver in Go and it uses decision diagrams[2].
Just today we launched our free cloud platform[0][1] which exposes our fleet routing model via an API. So if you’re curious about modern uses / systems around decision diagrams take a look at our site, app and blog[2].
Edit: did I misread the title the first time, or has it changed from “the last 20 years” to “the last 35”?
Chains of blocks and merkle trees are distinguishable from linked lists and binary trees purely by the use of hash functions instead of pointers. But that turns out to be really powerful in a way that the pointer versions aren't, if those hash functions are cryptographically secure.
SHA256 meanwhile was introduced in 2001, and since then no significant attacks have been found. So not only has it withstood attack for much longer, cryptography has advanced greatly compared to what we knew in 1992.
That still isn't a guarantee of future success. But look at it this way: I don't think you could have introduced Bitcoin in 1998. Hash functions were just too new to be trusted to the extent that Bitcoin requires.
In fact bitcoin is a pretty good counter-example to your point. It was launched too early, with a poor hash function[1], and yet is still a success.
[1] because bitcoin didn't used a brute-force resistant hash function, Satoshi's dream of “everyone is a miner” quickly disappeared a was replaced by a monopolistic cartel of professional miners.
Exactly. Collision attacks are fatal to Bitcoin, because they can make it impossible to achieve consensus over what is the valid version of the blockchain data. If you get advanced warning, transition is possible with some caveats. But hoping for advanced warning is risky when money is on the line (collision attacks can even be used to steal money in certain scenarios, eg with certain ways of doing multisig).
> because bitcoin didn't used a brute-force resistant hash function
That's really a topic in of itself. There is no such thing as a non-"brute-force-resistant" PoW function.
> There is no such thing as a non-"brute-force-resistant" PoW function.
Well, maybe on the semantic debate, but there's a big difference between fast hash functions (sha-2 and the likes) and slow-by-design ones: ASIC.
I hope that it's an intentional joke.
The set of all elements under consideration. It's a common term in math.
Maybe the Wikipedia page is a better start. Or maybe a blogpost out there is a better description of BDDs.
-------
Okay, so what is a BDD? Lets start with what problem we're trying to solve.
https://www.hillelwayne.com/post/decision-table-patterns/
"Decision Tables are useful". Lets start with that. They're useful in a variety of algorithms and situations. The above blogpost is your "ELI5" introduction to this subject.
Now lets start talking HARD problems, I'm talking NP-hard, like traveling salesman. We can use "decision tables" to decide if "CityA + CityB" should be in a certain order in the path, or if it should be "CityB -> CityA", and the like. Ultimately, its all a table of decisions, but this table starts getting big. Very, very, very big.
Exponentially big even. Every "column" you add doubles the size of the table. We can't fundamentally get around this, but we can offer a kind of "compression". Lets start with a 3-bit table and think about things.
ABC | True / False bit
----+-----------
000 | 1
001 | 0
010 | 0
011 | 0
100 | 1
101 | 1
110 | 1
111 | 1
ABC | True / False bit
----+-----------
000 | 1
001 | 0
01* | 0
1** | 1
Now Binary Decision Trees are a compression methodology. Instead of storing a table, you store a graph. One such graph is...
A=1 -> 1
A=0 -> B=1 -> 0
A=0 -> B=0 -> C=0 -> 1
B=0 -> C=1 -> 0
Ultimately: that's the goal. To "compress" these tables so that they take up less RAM. But we still want to perform operations on them (such as AND/OR/NOT, but also cross-joins and a bunch of relational-algebra). The overall discovery was that the graph-form, the Binary Decision Tree, is actually pretty efficient with a large number of operations.
----
EDIT: Ah right. And the "key feature" of BDDs is the ability to share "subtables" between different tables. Notice that B=0 has two links, so there is substantial "column-savings" compared to the original table.
The "compressed table" had to store 000 and 001 in two different rows. But the A=0 -> B=0 link is "redundant information" in that situation, and itself can be compressed.
The graph form compresses that information, while the "compressed table" doesn't. These small savings don't matter on 3-bit examples. But on a 16-bit or 32-bit or larger graph, those sorts of things really add up to huge amounts of compression.
And once you start sharing subtables among "unrelated" tables (ex: lets say you have 100-such tables. The graph form provides an obvious "common subtable" that can be shared between say 20+ tables at a time. The "compressed table" cannot share such subtables in any obvious way).
You don't want to go too crazy: the optimal sub-table compression is itself an NP complete problem. But don't worry about that: this is quite common on NP-hard situations. You need to solve NP-hard subproblems to solve the greater NP-hard problem efficiently...
Instead, find a greedy, "decent" solution to compression. Simple heuristics (column ordering heuristics, variable-ordering heuristics, etc. etc.) and the like are common here. As long as it works kinda-sorta okay, you're probably fine.
Ehh, I've got it close enough at this point. Its no where near a rigorous description of BDDs, but... sometimes an inaccurate but simple explanation is more useful than a fully accurate description.
In his video lecture Fun With Binary Decision Diagrams (BDDs),[8] Donald Knuth calls BDDs "one of the only really fundamental data structures that came out in the last twenty-five years" and mentions that Bryant's 1986 paper was for some time one of the most-cited papers in computer science.
See also: https://stackoverflow.com/questions/33510897/is-it-possible-...
2011 https://news.ycombinator.com/item?id=2477011 (a bit)
2010 https://news.ycombinator.com/item?id=1335740 (even less, but good)
Put them in a set(), then iterate over its members and report any that contain b and are still in the set after the string replacement. O(n), which can't be beaten.
Edit: If you're downvoting, could you post a comment saying why?
You’re right to think this is impossible though. Grover’s algorithm was one of the first examples of something that clearly could not ever exist classically.
So you fill the set with in O(1*N), again loop through the (original?) list assuming its O(N) to do so searching the set for replacements?
So at least a few passes through every element.
You could actually reduce this by excluding elements as you insert. You don't need to fill your search space with with anything that has a "b" for example, eliminating inserts.
I'm not sure that works. Suppose "abab" and "abao" are words. Note the problem spec says "after replacing a b with an o", i.e. after replacing _one_ b in a word with an o. If you exclude all words with a "b" and replace one b with an o in "abab" you will get "abao" which you have excluded, so you will think it's not a word. I think at best you can ignore only words with a single b.
However you can skip words that started with no Bs as clearly still being words without a search and you can remove search words with no Os.
That is, if Ws is the set of 5-letter words we want the set Rs = {w: w ∈ Ws, w.replace(b,o) ∈ Ws}. You can see that that's an O(n²) operation (each ∈ is an iteration over Ws).
jayd16 proposed omitting every word that has a b in it from the "search space". I take this to mean, in practice, that we start by initialising a set Ss = {w: w ∈ Ws, b ∉ w}. Then Rs = {w: w ∈ Ws, w.replace(b,o) ∈ Ss} and the time complexity is O(|Ws||Ss|) which is again O(n²) in the worst case (where Ws = Ss). Note also that some words in Ws may have more than one b and since we are only replacing "a b" (i.e. one b) we may remove valid words this way.
In any case, I don't see an obvious way to do this in O(n). Maybe I'm not thinking straight though, it's way past bed time.
In any case, even if it was O(n²) that's a polynomial time complexity and I don't see why BDDs are needed.
More, an O(n) algorithm can be more "efficient" than an O(lg(n)) one, for some values of n. (Or just in another facet. Maybe you actually do care about space.)
The claim wasn't how to do it fast, per se. It was how to do it efficiently. And comparing two algorithms of the same order can have a wide difference in the answer.
This can directly represent a regex with | operators but not Kleene star. The DD canonicalization automatically makes this structure share suffixes, but not prefixes.
So these “BDDs” allow for “efficient” solutions to the traveling salesman problem? Call me a skeptic, but I’m skeptical...
For example, the first computation of the exact number of closed knight tours on an 8x8 chessboard was done in 1996 using BDDs. (Their program actually had a bug which they corrected later and in the meantime another method gave the correct answer, but the method itself was sound.)
It's indeed true that the travelling salesman problem (TSP) is a “hard problem” in the sense of being NP-complete. But this implies only that no algorithm is known whose running time grows polynomially as a function of the input size (as the size goes to infinity). The Concorde TSP Solver for instance has solved instances with as large as 85,900 vertices, and instances with about 50 vertices can be solved quickly even with simple branch-and-bound heuristics.
In this case (all the numbers in this paragraph are from Knuth's treatment in Volume 4A of TAOCP), the graph of the contiguous US states has 48 vertices and (it turns out each state has on average only a little over 4 neighbours) 105 edges. A Hamiltonian path is some subset of these edges that covers each vertex exactly once. What BDDs/ZDDs enable is to succinctly encode which of these 2^105 subsets are Hamiltonian paths—turns out it can be done with a data structure having 28808 nodes. Once you have constructed this data structure (ZDD), you can now answer many questions about this entire set of Hamiltonian paths (more quickly than you could by backtracking or similar): how many of them are there? (68,656,026.) How many are there that end in California? (2,707,075.) Which one is shortest (this is the standard TSP problem, for which there are many other methods) (11,698 miles), and which one is longest (18,040 miles)? What is the lexicographically first one (according to some order)? Can you quickly sample a path at random (such that each path is equally likely to be picked)? Etc.
For arbitrary worst-case input (which is what the NP-hardness of TSP is about), the corresponding BDD/ZDD may turn out to be too large, so we cannot do any of this efficiently. The magic is that in many cases of practical interest, we happen to get small BDDs. Knuth's treatment (57 pages of text, 22 of exercises, 58 of solutions) ends with a caveat that among other things points out:
> They apply chiefly to problems that have more solutions than can readily be examined one by one, problems whose solutions have a local structure that allows our algorithms to deal with only relatively few subproblems at a time.
As Knuth mentions, the 1986 paper that (re)introduced BDDs (ordered and reduced, as the term generally means today) was for many years the most-cited paper in computer science according to CiteSeer. It's very readable and mentions the advantages and disadvantages: https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf
BDDs allow for some formula manipulations that make it easy to devise "unbounded" model-checking (UMC) techniques (i.e., they can explore the full state space of a system). On the other hand, if you are only interested in a bounded exploration of the state space (i.e., check only those states that are at most "k" steps far from the initial state), then you can usually unroll the transition relation, encode it as a CNF formula, and just feed it to a SAT solver. This approach is usually faster than BDDs.
To extend SAT solvers to the UMC case, you have to either devise some tricks to do the aforementioned formula transformations with a SAT solver too, or use the solver to find an inductive argument (if the system is safe up to k steps, it will be safe up to k+1 step, for any k). This is known as k-induction.
Seminal papers in this field include:
J. R. Burch et al., “Symbolic model checking: 10^20 states and beyond,” in LICS 1990. doi: 10.1109/LICS.1990.113767. (BDD-based symbolic model checking)
A. Biere et al., “Symbolic model checking without BDDs,” in TACAS 1999. doi: 10.1007/3-540-49059-0_14. (SAT-based bounded model checking)
K. L. McMillan, “Applying SAT methods in unbounded symbolic model checking,” in CAV 2002. doi: 10.1007/3-540-45657-0_19. (SAT-based unbounded model checking)
M. Sheeran et al., “Checking safety properties using induction and a SAT-Solver,” in FMCAD 2000. doi: 10.1007/3-540-40922-X_8. (k-induction)
You'd probably use BDD in a SAT solver. BDDs grossly cut down on the storage requirements of your variables and their possible "true/false" states... while almost all SAT-based math (union, intersection, etc. etc.) remains efficient.
BDDs aren't the only datastructure (ex: a B-Tree could beat a HashSet in a Database). But BDDs are a very, very good data-structure for SAT.
Uhm, I'm not sure about that. Most state-of-the-art SAT solvers nowadays will rely on CDCL [0], which does not need BDDs. A recent paper [1] is quite clear on that:
> The Conflict-Driven Clause Learning (CDCL) solvers form the core of the algorithms for solving the Boolean satisfiability problem (SAT).
There is a huge slide deck [2] which contains (in the first part) a lot of details about modern SAT solving. Highly recommended reading for those interested.
[0]: https://en.wikipedia.org/wiki/DPLL_algorithm
[1]: https://link.springer.com/chapter/10.1007%2F978-3-030-51825-...
[2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo...
A BDD can also efficiently answer questions like "how many ways can you satisfy this formula?" (subject to the same caveat about problem suitability).
Sadly, variable ordering is NP-Hard. This is brutal for static analysis applications where BDDs seem like they are going to save the world but often end up crushing dreams.
it's really amazing what you can do with it.
B-epsilon trees: These allow asymptotic speedups for insert/update/delete operations on search trees in external memory (Introduced in 2002 by the paper, Lower Bounds for External Memory Dictionaries)
Cache-Oblivious B-Trees: This is an external-memory search tree that exhibits optimal behavior on a cache with any (possibly unknown) cache-size and cache-line size parameters. (Introduced in 2000 by the paper Cache-Oblivious B trees)
Fusion trees: This allows for search operations in a small binary tree (i.e., a tree whose size is polynomial in the machine word size) to be performed in constant time, rather than logarithmic time. (Introduced in 1990 by the paper Blasting through the Information Theoretic Barrier with Fusion Trees.)
Cuckoo hashing: This is a hash table design introduced in 2001. In 2009, the paper De-amortized Cuckoo Hashing showed how to make all operations in Cuckoo hashing take truly constant time with high probability. This remains (as far as I know) the only known technique for guaranteeing constant-time operation for a hash table without the use of bit manipulation tricks or the method of four Russians.
These are just examples off the top of my head. I'm sure there are many more.
Edit to add: I’m not a Clojure expert, but I believe you could trace a direct line to Clojure’s core immutable data structures from Okasaki’s doctoral thesis. But maybe I’m wrong! Would love to hear about another other takes on this or links to other research strands I’m not aware of.
> I’m not a Clojure expert, but I believe you could trace a direct line to Clojure’s core immutable data structures from Okasaki’s doctoral thesis.
I believe the direct inspiration for Clojure's persistent vectors and maps are Bagwell's papers on HAMTs, which weren't so much a new data structure as an example of data structure engineering. Okasaki's thesis has several contributions but its main theme is how you can apply amortization in the purely functional setting if you have laziness or memoization, which is in a very different direction.
On another note: what are some amazing things you can do with it?
While with Karnaugh maps you can simplify a boolean function with a few variables, BDDs can solve for thousands, fast.
And no need to explain applications of high-dimensional boolean algebra on HN, with boolean algebra you can solve any logic problem expressed as boolean function, any combinatorial problem (except for those with nasty functions), classic graph theory problems.
Surprisingly it allows to solve optimization problems[4], like boolean programming, SAT solver, max independent set or max cut in graphs, very efficiently, it can be used in something like belief propagation or lattice induction for inference, but if that's not enough you can use it for random number generation, lossless compression, perfect hashing, etc, etc.
I haven't seen such a versatile data structure elsewhere, most of the other things developed in the last 35 years, like the ones in the comment below are solving special cases, BDD is truly one of the most fundamental and severely underrated "swiss army knives" (that is in CS, EE people know it very well in logic synthesis and verification, BDD's first "killer app").
It's probably easier to list what you can't do with BDD, kind of like what you can't do with (high-dimensional) boolean logic.
I think it skipped the radar of CompSci community at large because it was too quickly siloed into "that circuit analysis/verification tool used by electrical engineers".
Yes, it's "just" a DAG but with very particular (and very simple) constraints which allow it to solve infinite variety of problems in a very elegant and surprising way [5].
[1] it's really worth watching the lecture on BDDs by Don Knuth , starting around 13:32, his enthusiasm is contagious: https://www.youtube.com/watch?v=SQE21efsf7Y&t=13m32s
Part 2 on ZDD: https://www.youtube.com/watch?v=-HzQYeqS9Wc
[2] TAOCP, volume 4A, Combinatorial Algorithms, p.202 - 280: https://www.amazon.com/Art-Computer-Programming-Combinatoria...
There is a free preprint here https://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz
[3] https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagr...
[4] Bergman, David, et al. "Discrete optimization with decision diagrams." INFORMS Journal on Computing 28.1 (2016): 47-66.
[5] Bryant, Randal E. "Graph-based algorithms for boolean function manipulation." Computers, IEEE Transactions on 100.8 (1986): 677-691.
I hope that answers your question, dang, and sorry for title mishap.