| The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability (Addison-Wesley) |
| Monday, 20 June 2016 | |||
This is the latest chunk in Donald Knuth's epic multivolume work on the analysis of algorithms. For it's history see Donald Knuth and the Art of Programming. To continue the 4th and later volumes of the set, and to update parts of the existing volumes, Knuth has created a series of small books called fascicles, which are published at regular intervals and cover distinct topics - in this case Satisfiability.. Satisfiability is far from an abstract exercise in understanding formal systems. Revolutionary methods for solving such problems emerged at the beginning of the twenty-first century, and they’ve led to game-changing applications in industry. These so-called “SAT solvers’’ can now routinely find solutions to practical problems that involve millions of variables and were thought until very recently to be hopelessly difficult. Fascicle 6 presents full details of seven different SAT solvers, ranging from simple algorithms suitable for small problems to state-of-the-art algorithms of industrial strength. Many other significant topics also arise in the course of the discussion, such as bounded model checking, the theory of traces, Las Vegas algorithms, phase changes in random processes, the efficient encoding of problems into conjunctive normal form, and the exploitation of global and local symmetries. More than 500 exercises are provided, arranged carefully for self-instruction, together with detailed answers. Author: Donald E. Knuth
The Art of Computer Programming, Volume 4, Fascicle 1 (book review) Donald Knuth and the Art of Programming Another Chunk of The Art of Computer Programming
Visit Book Watch Archive for hundreds more titles. Follow @bookwatchiprog on Twitter or subscribe to I Programmer's Books RSS feed for each day's new addition to Book Watch and for new reviews. To have new titles included in Book Watch contact BookWatch@i-programmer.info
|