CIS1921 - Lecture 4 - Backjumping, Implication Graphs, CDCL

Lecture 4 wraps up our discussion of SAT. We explore some of the more modern advancements in SAT solvers such as backjumping, which is accomplished through implication graphs, conflict sets, and the 1-UIP schema. These techniques combine together to create the Conflict Driven Clause Learning (CDCL) algorithm, which was introduced by the GRASP solver in 1996, and inspired many other SAT solvers that came thereafter. Presenter: Ishaan Lal Lecture Date: 9/19/2024