Don Knuth previews chapter 7 of volume 4 of his legendary Art of Computer Programming. post 
quote
The middle third of Volume 4B will be a major introduction to the topic of Boolean Satisfiability, emphasizing its many applications, together with a variety of algorithms to solve SAT problems with greater and greater speed.
I began studying this topic in autumn 2011, and found it to be amazingly interesting. So I've had great fun telling this story, and connecting SAT with many other aspects of computer science and math.
It's not a short story; indeed, this section has turned out to be the largest by far of any in The Art of Computer Programming. But the material is rich, beautiful, instructive, and important, so I'm pleased to have had the opportunity to pull it together from many sources.
Here then, ta-da, is the current draft of pre-fascicle 6a (317 pages). This is revision 0, dated 01 July 2015. It includes 525 exercises and a comprehensive index. I'm putting it online now for beta-testing; Addison-Wesley plans to publish it in paperback before the end of 2015. Happy reading!
postscript
.
Don shows us that many important programming problems can be reduced to the simple question, is there any combination of variable values that makes a particular boolean expression true? And, more importantly, this question, though notoriously difficult, has solvers that produce good results on practical computers.
Don also shows how a deep thinker can express himself on the computer generated printed page. If federated wiki needs a counterpoint then this is it.