The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability (Paperback)

This multivolume work on the analysis of algorithms has long been recognized as the definitive description of classical computer science. The four volumes published to date already comprise a unique and invaluable resource in programming theory and practice. Countless readers have spoken about the profound personal influence of Knuth’s writings. Scientists have marveled at the beauty and elegance of his analysis, while practicing programmers have successfully applied his “cookbook” solutions to their day-to-day problems. All have admired Knuth for the breadth, clarity, accuracy, and good humor found in his books.

To continue the fourth 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. Each fascicle encompasses a section or more of wholly new or revised material. Ultimately, the content of these fascicles will be rolled up into the comprehensive, final versions of each volume, and the enormous undertaking that began in 1962 will be complete.

Volume 4 Fascicle 6

This fascicle, brimming with lively examples, forms the middle third of what will eventually become hardcover Volume 4B. It introduces and surveys “Satisfiability,’’ one of the most fundamental problems in all of computer science: Given a Boolean function, can its variables be set to at least one pattern of 0s and 1s that will make the function true?

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.

這部關於算法分析的多卷作品長期以來一直被認為是經典計算機科學的權威描述。迄今為止已經出版的四卷已經成為編程理論和實踐中獨特且寶貴的資源。無數讀者談到了Knuth的著作對他們的深遠影響。科學家對他的分析的美麗和優雅感到驚嘆，而實踐編程人員則成功地將他的“食譜”解決方案應用於日常問題。所有人都欣賞Knuth在他的書中所展現的廣度、清晰度、準確性和幽默感。

為了繼續完成這套書的第四卷和之後的卷，並更新現有卷的部分內容，Knuth創作了一系列稱為fascicles的小書，定期出版。每個fascicle都包含一個或多個全新或修訂的部分。最終，這些fascicles的內容將被整合到每個卷的全面最終版本中，這項從1962年開始的巨大工程將會完成。

這本fascicle充滿了生動的例子，它是最終將成為硬皮書第4B卷的中間部分。它介紹並概述了“可滿足性”，這是計算機科學中最基本的問題之一：給定一個布爾函數，是否可以將其變量設置為至少一個使函數為真的0和1的模式？

可滿足性遠非一個理解形式系統的抽象練習。在21世紀初出現了解決這類問題的革命性方法，它們已經在工業界引起了改變遊戲規則的應用。這些所謂的“SAT求解器”現在可以常規地找到涉及數百萬變量且在不久前被認為是無望困難的實際問題的解決方案。

第6本fascicle詳細介紹了七種不同的SAT求解器，從適用於小問題的簡單算法到工業強度的最先進算法。在討論過程中還涉及許多其他重要主題，例如有界模型檢查、蹤跡理論、拉斯維加斯算法、隨機過程中的相變、將問題高效編碼為合取范式以及全局和局部對稱性的利用。提供了500多個練習題，精心安排供自學，並附有詳細答案。