I attended one of his talks (but not the ones you mention), during which he described how he was approaching the topic. He said he was reading the most important papers on sat problems in chronological order, and implementing each of the algorithms he found along the way. At the time of the talk, he was half-way through the ‘80s, IIRC.
A lesson in commitment and perseverance for me. And a very funny talk as well (Knuth likes jokes!)
His programs (SAT solvers) are also available on his site at https://cs.stanford.edu/~knuth/programs.html (They are in CWEB and you'll have to use cweave and ctangle to read and run those programs respectively; if you just want to read I've typeset them here: https://github.com/shreevatsa/knuth-literate-programs/tree/1...)
Knuth has also given a couple of talks about satisfiability around the time he wrote the book:
- https://www.pathlms.com/siam/courses/3028/sections/4140/vide... (July 2016, at SIAM Annual Meeting)
- https://www.youtube.com/watch?v=g4lhrVPDUG0 (December 2016, at Brown University)
Look at https://cs.stanford.edu/~knuth/news16.html#lectures for slides and handouts from these talks.