Open Collections

Description

This talk presents a brief yet fresh introduction to SAT solving before surveying recent developments in the field. We introduce core SAT as resoluting backtrack search, presenting BCP and 1UIP learning without implication graphs. We then survey recent advances in sequential SAT solving. First, we examine SAT Competition winners from 2021–2025, with particular focus on the LLM-empowered 2025 winner AE-Kissat-MAB and its predecessors. Then, we explore developments in SAT beyond competitions, including API extension for broader applicability (IPASIR-UP), domain-specific SAT solving for IC3 (GipSAT), and chronological backtracking's impact on enumeration, model counting, and its promise for SAT applications.