[Proof Complexity] MIAO seminar Mon Jun 1 at 14:00 CEST with Alexander Nadel: SAT solving and beyond: A fresh intro and recent developments

[Jakob Nordström]

Dear all,

On Monday June 1 at 14:00 CEST, we will have the opportunity to listen to an in-depth presentation of modern Boolean satisfiability (SAT) solving, which has revolutionized the area of combinatorial solving since the turn of the millennium. Alexander Nadel from Nvidia and the Technion – Israel Institute of Technology, one of the leading experts in this area, will give a talk titled "SAT solving and beyond: A fresh intro and recent developments". You find the abstract at the bottom of this message.

This will be a video seminar at https://lu-se.zoom.us/j/61925271827 . We are expecting a slightly longer, tutorial-style, talk, which might be closer to the 2-hour than the 1-hour mark. However, we will take a break halfway through, and the first part will hopefully be a self-contained overview of modern SAT solving. And, as always, it will be perfectly fine to just discretely drop out during the break. No questions asked, no excuses needed.

Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend (in which context it is worth noting that Alexander Nadel's presentation on the Intel SAT solver https://youtu.be/ZF-fvMfPYGs from a few years back is one of the absolutely most popular videos of the channel).

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Monday Jun 1 at 14:00 on Zoom
*SAT solving and beyond: A fresh intro and recent developments
*(Alexander Nadel, Nvidia & Technion)
/
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 (SC) winners from the very first competition to 2025, with a particular focus on the last 5 years, including the LLM-empowered latest SC winner AE_kissat2025_MAB. 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. Finally, we discuss the solution generalization hierarchy, demonstrating that CNF-level generalization is outperformed by circuit-level approaches, which are in turn surpassed by dual (negated) circuit-based methods.

This is an extended version of a talk given at the BIRS workshop /Theory and practice of SAT and combinatorial solving /(https://www.birs.ca/events/2026/5-day-workshops/26w5626/) in January 2026.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se