Knuth recently just put out a draft of his section on satisfiability (section 7.2.2.2, available here: www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz), and there they are, Gosper and Schroeppel referenced in the answers to the exercises, page 60. Here's the excerpt (as an image): [SPOILER, answer to exercise 9d] http://i.imgur.com/IXSIH.png [/SPOILER] Three cheers for HAKMEM! -Robert