DPLL and CDCL SAT solving from first principles. Understand unit propagation, conflict analysis, clause learning, and non-chronological backtracking — the core of every modern solver.
Part of Decision Procedures for Hardware Formal Verification on formal.org.