3 ms·

One impressive application of these is counting state spaces. In [1], Stefan Edelkamp and Peter Kissmann count the number of connect-4 positions: > Symbolic s

by 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.
boothby 4y ago
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 https://oeis.org/search?q=1104642469

by tromp 4y ago

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.

boothby 4y ago

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 https://oeis.org/search?q=1104642469