8 ms·
I, unfortunately, cannot find an online copy currently. Knuth's TAOCP's latest published part, Volume 4 Fascicle 6, on Satisfiability contains a number of visu
by Phemist 4y ago
I, unfortunately, cannot find an online copy currently.
Knuth's TAOCP's latest published part, Volume 4 Fascicle 6, on Satisfiability contains a number of visualizations that really are amazing and worth just buying a copy of the book for, just to ponder over these images.
The satisfiability problem of whether there exists an assignment of boolean values that makes a given boolean formula evaluate to TRUE is, IMO, truly a fundamental problem in computer science.
Any piece of code with some inputs and outputs can be transformed into a boolean formula (albeit a huge one). This process feels akin to expressing molecules, from simple ones like H2O, to the highly complex proteins that make up much of our Cells, in their constituent atoms and more importantly the atom interactions.
Knuth (EDIT: Actually, Carsten Sinz) takes this concept one step further and produces visualizations of non-trivial boolean formulas that clearly show the regular, both symmetrical and asymmetrical, sometimes fractal-like nature of these formulas.
In my mind, these visualizations are quite powerful and strikingly show the fundamental building blocks of (digital) computation.
- varjag 4y agoThe spread on page 300 (iirc) is really stunning.
- LeonM 4y agoImage here: https://imgur.com/a/auDF9qh https://imgur.com/a/auDF9qh
- radec 4y agoCleaner image https://imgur.com/a/lPPpT3L https://imgur.com/a/lPPpT3L
- eurasiantiger 4y agoThese seem to have structural parallels to Wolfram’s classification of cellular automata.
- Eduard 4y agoPDF: https://kolegite.com/EE_library/books_and_lectures/%D0%9F%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%B8%D1%80%D0%B0%D0%BD%D0%B5/The%20Art%20of%20Computer%20Programming%2C%20Volume%204%2C%20Fascicle%206%20Satisfiability%20%28Donald%20E.%20Knuth%29%20%28z-lib.org%29.pdf https://kolegite.com/EE_library/books_and_lectures/%D0%9F%D1... Physical pages 116-117; PDF pages 126-127.
- sacnoradhq 4y agoAlso 4B (1st ed) pp. 300-301. ProTip: Order the 5 vol set directly from Addison-Wesley, it's much cheaper than anywhere else.
- Eduard 4y ago> Knuth takes this concept one step further and produces visualizations of non-trivial boolean formulas that clearly show the regular, both symmetrical and asymmetrical, sometimes fractal-like nature of these formulas. The visualizations were done by Carsten Sinz. This is his paper describing the technique: Carsten Sinz. Visualizing SAT Instances and Runs of the DPLL Algorithm. J. Automated Reasoning, 39(2):219-243, 2007. https://www.carstensinz.de/papers/JAR-2007-Visualization.pdf https://www.carstensinz.de/papers/JAR-2007-Visualization.pdf https://doi.org/10.1007/s10817-007-9074-1 https://doi.org/10.1007/s10817-007-9074-1
- Phemist 4y agoAha! I have edited my post. Thanks for the correction! Beautiful work, looks like something I'd like to play around with as well :)
- piyush_soni 4y agoAnd that's why I love HN! (sorry for a non-contributing post).
- k0k0r0 4y agoI am lucky to be paid to work on SAT. I wouldn't yet say I am an expert, yet, but it is really a pleasure to do so. Trying to improve on algorithms to solve these problems is truly humbling. Edit: Fixed a typo.
- Phemist 4y agoIm jealous! To me, from the sidelines, people working on SAT are like the experimentally-focused particle physicists of computer science.
- puglr 4y agoWow, you weren't kidding about those images. What I found particularly striking about them was how much they reminded me of both neurons and larger brain structures, as well as some of those newer, ML-assisted FMRI imagery. Probably just coincidence and wishful thinking, but it instills a sense of daydream-like wonder all the same.