Model checking of finite state transition systems has interesting applications in hardware verification. Boolean satisfiability (SAT) algorithms have proven to be very effective for this purpose. This paper captures the trends of the SAT applications in model checking. For practitioners interested in an overview of recent advancements in this technology, this paper offers a good summary.

The paper provides the relevant background material and quickly moves on to the details. Adequate references are provided for further understanding. Although the material is well organized and well presented, Marques-Silva does not attempt to make a comprehensive survey. As a result, several details are omitted from the discussion.

The author first introduces the notation used and describes the conflict-driven clause learning (CDCL) algorithm. Although the author mentions that alternative algorithms exist for the SAT problem, no further pointers are provided. Next, the author describes resolution proofs and “interpolant” computation. These concepts provide the necessary material for the model-checking application.

The remainder of the paper is devoted to describing model-checking algorithms using SAT. Algorithms for both bounded model checking (BMC) and unbounded model checking (UMC) are provided.

The paper is interesting to read and presents methods that are already proven in the industry. However, it does not narrate the limitations of these approaches. Also, there are no suggestions on open problems in this area, so researchers may not find any new insights.