When the first edition of this handbook was published in 2009 advances in SAT were mostly only known to experts, and SAT was seen as a key technology only in certain applications. Since then the number of practical applications has exploded, along with greater awareness of the usefulness of SAT in general: In the last century showing that a certain problem is as hard as SAT was the end of the story and trying to solve it directly seemed to be hopeless. Relying on the continuing improvements made in practical SAT solving, it is now widely accepted that being able to encode a problem into SAT also is highly likely to lead to a practical solution. This “SAT Revolution” started at the end of the last century and continues to produce amazing new practical and theoretical results.

Accordingly, this second edition contains several updates, including a completely revamped Chapter 4 on conflict-driven clause learning. Half the chapters were updated or extended or both. Comments by Donald Knuth were also taken into account, collected while he was preparing the Section on Satisfiability in volume 4 of the “The Art of Computer Programming”. This section appeared as fascicle 6a with more than 300 pages in 2015 and is a major milestone in the SAT literature that has appeared since the first edition of this Handbook.

Three important topics, which were already in the first edition of the handbook and deserve their own chapter, are now given enough space and discussed in detail: there is the new Chapter 7 on proof complexity, Chapter 9 on preprocessing, as well as the new Chapter 12 on automated configuration and solver selection. Additionally, the new Chapter 15 covers proofs of unsatisfiability, one of the main recent developments in practical SAT solving. These proofs are essential in solving long-standing mathematical problems.

Beside these four completely new chapters, there are three new chapters which cover topics already discussed in the first edition. These three chapters focus on new aspects and new technology and are written by authors who made fundamental contributions to change the state of the art. First, recent developments regarding quantified Boolean formulas including the discussion of proof systems are covered in the new Chapter 31. Second, the focus of the new Chapter 24 is on core-based methods for maximum satisfiability which have improved scalability considerably. Finally, the last new Chapter 26 covers a novel research direction on practical and approximate model counting with strong statistical guarantees.

Research in SAT has established itself as a vibrant cross community effort. Beside the main SAT conference, other major conferences and journals in diverse fields from automated reasoning, verification, hardware to software engineering, complexity theory, even algorithms and of course artificial intelligence cover SAT and its extensions areas of interest. It is also worth mentioning that competitions continue to serve as a show case as well as motivation of the field.

One could argue that SAT is now very widespread across these fields. As one example, and maybe most striking, is the adoption of SAT in other reasoning disciplines, starting of course with SMT solving, the use of lazy clause generation in constraint programming, as well as SAT based splitting in first-order theorem proving, and finally in the use of hammers in interactive theorem proving for higher-order logic relying directly or indirectly on SAT.

As the first edition appears to have done, we hope that also this second edition of the Handbook will serve researchers and practitioners using or contributing to SAT, and provide both an inspiration and a rich resource for their own work.

Armin Biere

Marijn Heule

Hans van Maaren

Toby Walsh