SIAM News Blog

Knuth Gives Satisfaction in SIAM von Neumann Lecture

By Nicholas Higham

Donald Knuth of Stanford University gave the John von Neumann Lecture at the 2016 SIAM Annual Meeting in Boston.
Donald Knuth, Professor Emeritus of the Art of Computer Programming at Stanford University, gave the John von Neumann lecture at the 2016 SIAM Annual Meeting in Boston. The von Neumann lecture is SIAM's most prestigious prize and was awarded to Knuth in recognition of his "transformative contributions to mathematics and computer science". These contributions lie in areas including the mathematical analysis of algorithms, programming languages, and the development of the typesetting system TeX. Referring to the latter, Cédric Villani, in his recent book Birth of a Theorem, says that "Knuth has probably done more than any other living person to change the daily working lives of mathematicians".

Knuth based the lecture, titled "Satisfiability and Combinatorics", on the latest part (Volume 4, Fascicle 6) of his The Art of Computer Programming book series. He showed us the first page of the fascicle, aptly illustrated with the quote "I can't get no …" from the Rolling Stones. In the preface of the fascicle Knuth says "The story of satisfiability is the tale of a triumph of software engineering, blended with rich doses of beautiful mathematics".

The satisfiability problem (or SAT) is to check whether a logical formula expressed in Boolean algebra can evaluate to true when its variables are consistently replaced by true or false. Knuth began by describing the history of the problem, following a trail that included Quine (1940), Davis and Putnam (1960), Cook (1971), Brown and Purdom (1982), and a team of seven who won the 2009 Computer-Aided Verification award for their high performance SAT solver. He discussed the relation with complexity theory, noting that the SAT problem is NP-complete, as proved by Cook in his ground-breaking 1971 paper on the P versus NP problem.

Knuth is a strong advocate of literate programming, in which program code and documentation are intermingled, and he commented that it is one of the main things that he has taken from his work on TeX. Practising what he preaches, he described a series of literate programs he has written to solve the satisfiability problem.

Donald Knuth validating the solution to his puzzle by two young problem solvers. Photo credit: Des Higham.

During the talk Knuth harked back to Conway's Game of Life—a golden oldie from the 1970s that was perhaps unknown to some of the younger attendees. He demonstrated how the inverse problem of finding a population to generate a given pattern could be attacked using satisfiability techniques.

On entering the room the audience members had been handed a folded piece of paper that they were instructed not to unfold until Knuth gave the word. When he did so, towards the end of the talk, delegates saw "A Digital Tomography Puzzle", which required a 7-by-21 array of squares to be filled in black or white to match specified row, column and diagonal sums of black cells. The puzzle proved popular not just with the professionals in the audience but also with a couple of budding grade 7 and 8 mathematicians who had their solution verified by Knuth at the poster session.

Unlike the Rolling Stones, the packed audience certainly did get satisfaction, thanks to Knuth's entertaining and informative tour through this fascinating combinatoric problem.

   Nicholas Higham is the Richardson Professor of Applied Mathematics at the University of Manchester. He is President Elect of SIAM. 
blog comments powered by Disqus