1 of 82

SAT Solving: �A Fresh Intro and Recent Developments

Alexander Nadel

Technion, Data and Decision Sciences & NVIDIA, Israel

January 12, 2025

BIRS Workshop "Theory and Practice of SAT and Combinatorial Solving"

Banff, Alberta, Canada

1

2 of 82

The SAT Problem

SAT: is a Boolean formula in Conjunctive Normal Form (CNF) satisfiable?

Theory: The original NP-Complete problem

The famous Cook-Levin theorem (early 70s)
SAT has exponential complexity unless P = NP

P = NP: frequently called the most important outstanding question in CS
One of the 7 unsolved Clay Millennium Prize Problems – worth $1,000,000
The essence:

It is aways easy to verify a given solution
Is there an easy way to solve any given problem?

Today’s practice:

Modern SAT solvers handle huge industrial problems (hundreds of millions of clauses)
Apps: HW&SW Validation, AI, Scheduling, Combinatorics, Cryptography, Biology…

Gap between theory and practice!

2

F = (a ∨ b) ∧ (¬a ∨ ¬b ∨ c)

clause #1

clause #2

Literals

3 of 82

Agenda

Introduction: core SAT as resoluting backtrack search

BCP & 1UIP learning without implication graphs

What’s new in (sequential) SAT solving

Reviewing SAT Competition winners during 2021–2025, focusing on:

The LLM-empowered SC’25 winner AE-Kissat-MAB and its heuristic predecessors

Extensions & applications beyond SAT Competitions

Hooks into SAT for broader applicability (IPASIR-UP)
Domain (IC3)-dedicated SAT solving (GipSAT)
Chronological backtracking for extensions & apps: the promise and delivery so far

3

4 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

5 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

6 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a’

7 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a + b

a’

b’

8 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a + b

a’

b’

b

9 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

a’

b’

b

c’

10 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

11 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

b’

b

c’

c

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

b’ + c’

a’

a

12 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

a’

a

b

b’

b

c’

c

a + b

b’ + c

b’ + c’

13 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

a’

a

b

c’

b’

b

c’

c

a + b

b’ + c

b’ + c’

14 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a + b

b’ + c

b’ + c’

15 of 82

SAT Foundations: Backtrack Search or DPLL�Martin Davis, George Logemann, Donald Loveland: A Machine Program for Theorem Proving. Comm. ACM 5 (7), 1962.�Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7 (1), 1960.

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a + b

b’ + c

b’ + c’

a’ + b

b’

UNSAT!

16 of 82

Core SAT as Resoluting Backtrack Search or �From Backtrack Search to CDCL without Implication Graphs�

Boolean Constraint Propagation (BCP)

Apply unit clause rule till fixed-point:

Original DLL paper

BCP is but a branching heuristic!
Whenever a unit clause exists 🡪 assign c₁’
BCP is a heuristic, but identifying falsified clauses isn’t

In modern solvers: 2 watches per clause isn’t a must, but one watch is!

1UIP Scheme for Clause Recording

Core of the CDCL breakthrough�João P. Marques Silva, Karem A. Sakallah: GRASP - a new search algorithm for satisfiability. ICCAD 1996.��Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver. DAC 2001.
Presented next:

Decision clause recording
1UIP clause recording

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a + b

b’ + c

b’ + c’

a’ + b

b’

c₂

c₁

c₃

c₂

c₁

c₃

Falsified literal:

Satisfied literal:

Unassigned literal:

c₂

c₁

c₃

17 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

18 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a’

19 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

a’

b’

20 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

a’

b’

A parent clause P(x) is associated with every flipped variable x. It contains:

The flipped literal of x
A subset of previously assigned variables, falsified

The parent clause justifies the flip proving that the explored subspace has no solutions

b

21 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

a’

b’

b

c’

22 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

a’

b’

b

c’

c

23 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

24 of 82

Core SAT as Resoluting Backtrack Search

Resolution over the pivot x:

a + b

b’ + c

b’ + c’

a’ + b

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

Backtracking over a flipped variable x can be associated with a resolution operation:

R := P(x) ⊕ R (clauses R are shown inside nodes)
R is to become the parent clause for the upcoming flip

R_old

P(c)

R_new

Y ∨ x

Z ∨ ¬x

Y ∨ Z

25 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

R_new

R_old

P(b)

Backtracking over a flipped variable x can be associated with a resolution operation:

R := P(x) ⊕ R
R is to become the parent clause for the upcoming flip

x∉R 🡪 R := R

Skip resolution

26 of 82

Core SAT as Resoluting Backtrack Search

x’

a + b

b’ + c

b’ + c’

a’ + b

a

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

R_new

R_old

Backtracking over a flipped variable x can be associated with a resolution operation:

R := P(x) ⊕ R
R is to become the parent clause for the upcoming flip

x∉R 🡪 R := R

Skip resolution

a’ + x

x

27 of 82

Core SAT as Resoluting Backtrack Search

x’

a + b

b’ + c

b’ + c’

a’ + b

a

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

R_new

R_old

Backtracking over a flipped variable x can be associated with a resolution operation:

R := P(x) ⊕ R
R is to become the parent clause for the upcoming flip

x∉R 🡪 R := R

Skip resolution

a’ + x

a

a’ + x

x

28 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

R_new

R_old

P(b)

Backtracking over a flipped variable x can be associated with a resolution operation:

R := P(x) ⊕ R
R is to become the parent clause for the upcoming flip

x∉R 🡪 R := R

Skip resolution

29 of 82

Core SAT as Resoluting Backtrack Search

b’

b

c’

c

a + b

b’ + c

b’ + c’

a’ + b

a

b’

a + b

b’ + c

b’ + c’

a’

a

Π(a)

The parent clause P(a) is derived by parent resolution Π(a).

30 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a’

a

b

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

31 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

a’

a

b

c’

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

32 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

P(c)

33 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

34 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

R_old

P(c)

R_new

35 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’

b’ + c

b’ + c’

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

Π(b)

36 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

b’

b’ + c

b’ + c’

a’ + b

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

37 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a’

b’

b’ + c

b’ + c’

a’ + b

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

R_old

P(b)

R_new

38 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

•

a’

b’

b’ + c

b’ + c’

a’ + b

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

R_old

P(a)

R_new

39 of 82

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

•

a’

b’

b’ + c

b’ + c’

a’ + b

a’

a

b

c’

c

b’

b

c’

c

a

b’

a + b

b’ + c

b’ + c’

The final trace of DPLL is both a decision tree (top-down view) and a resolution refutation (bottom-up view)

40 of 82

Decision Conflict Clause Recording

Record every parent clause to use it later for conflict detection

: recorded; : not recorded

Tree-like resolution 🡪 DAG resolution

40

41 of 82

1UIP Scheme

42 of 82

1UIP Scheme

1UIP scheme applies:

Stopping condition for backtracking:

Stop whenever R contains one variable of the last decision level, called the 1UIP variable

Rewriting: consider the 1UIP variable as a decision variable and R as its parent clause

a + b

b’ + c

b’ + c’

a’ + b

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

R

Starting with the latest unflipped variable

43 of 82

1UIP Scheme

a + b

b’ + c

b’ + c’

a’ + b

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

P

1UIP scheme applies:

Stopping condition for backtracking:

Stop whenever R contains one variable of the last decision level, called the 1UIP variable

Rewriting: consider the 1UIP variable as a decision variable and R as its parent clause

44 of 82

1UIP Scheme

a + b

b’ + c

b’ + c’

a’ + b

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

1UIP scheme applies:

Stopping condition for backtracking:

Stop whenever R contains one variable of the last decision level, called the 1UIP variable

Rewriting: consider the 1UIP variable as a decision variable and R as its parent clause

45 of 82

1UIP Scheme

a + b

b’ + c

b’ + c’

a’ + b

b’

a + b

b’ + c

b’ + c’

a’

b’

b

c’

c

1UIP scheme applies:

Stopping condition for backtracking:

Stop whenever R contains one variable of the last decision level, called the 1UIP variable

Rewriting: consider the 1UIP variable as a decision variable and R as its parent clause
Pruning: eliminate all the disconnected variables of the last decision level

46 of 82

1UIP Scheme

1UIP scheme applies:

Stopping condition for backtracking:

Stop whenever R contains one variable of the last decision level, called the 1UIP variable

Rewriting: consider the 1UIP variable as a decision variable and R as its parent clause
Pruning: eliminate all the disconnected variables of the last decision level

a + b

b’ + c

b’ + c’

a’ + b

b’

b’ + c

b’ + c’

b

c’

c

b’

Π(b)

47 of 82

Core SAT as Resoluting Backtrack Search: Final Thoughts

One can think of core SAT as resoluting backtrack search

Split on the way down, resolve on the way up

The fusion between backtrack search & resolution is mutually helpful

Resolution prunes the search space for backtrack search
Backtrack search serves as a heuristic for resolution to derive strong clauses
Could that be the secret behind the success of backtrack-search-based SAT?

47

48 of 82

SAT Competition Winners (Main Track -- Sequential & All-instances & Non-incremental)

48

Kissat-MAB: MAB heuristic to switch between EVSIDS and CHB – Stable (SAT) mode only

Kissat-MAB-HyWalk: combining multiple local search strategies

SBVA-Cadical: made BVA work

Kissat: clausal congruence closure; BVA; dynamic glue limit; revisited vivification

AE-Kissat-MAB: reintroduced MAB heuristic in Stable (SAT) mode with LLM-generated changes

Coming next:

Decision heuristic Clause management Inprocessing Reencoding Beyond resolution

2022

2023

2024

2025

Kissat-MAB

Cherif, Habet, Terrioux

2021

Kissat-MAB-HyWalk

Zheng, He, Chen, Zhou, Li

SBVA-Cadical

Haberlandt

Green

Kissat

Biere, Faller, Fazekas, Fleury, Froleyks, Pollitt

AE-Kissat-MAB

Ding, Luo,

C.M. Li, S. Li,

Chen,

Xiong, Wu

Relevant Heuristics Review

Kissat-MAB

AE-Kissat-MAB

49 of 82

Preliminaries: Kissat’s Variable Decision Heuristic & CHB

Kissat’s modes: Stable (SAT) and Focused (UNSAT)

Chanseok Oh: Between SAT and UNSAT: The Fundamental Difference in CDCL SAT. SAT 2015: 307-323

Stable (SAT) mode uses EVSIDS

Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518

Variables are stored in a score-based heap (priority queue)

Scores are bumped (score+= increment) when encountered in conflict derivation
increment grows exponentially

Decision: pick variable with the highest score
Locality principle: favors variables visited in recent conflicts

Focused (UNSAT) mode uses VMTF (Variable-Move-To-Front)�Lawrence Ryan: Efficient algorithms for clause-learning SAT solvers. Masters thesis, Simon Fraser University, February 2004

Variables are stored in a queue
Variables moved to the front when encountered in conflict derivation
Decision: pick the front variable
VMTF is EVSIDS on steroids - maximally aggressive locality

CHB Heuristic

Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. AAAI 2016: 3434-3440�

Tracks each variable's recent conflict involvement (similarly to EVSIDS)
Key difference from EVSIDS: uses exponential moving average (EMA) instead of additive bumping
Predecessor of LRB used in MapleCOMSPS (SC'16 winner)

49

50 of 82

Kissat-MAB: SC’21 Winner�Mohamed Sami Cherif, Djamal Habet, Cyril Terrioux: Combining VSIDS and CHB Using Restarts in SAT. CP 2021.

The essence: integrated CHB-based heuristic into Kissat (stable (SAT) mode only)

Problem: neither EVSIDS nor CHB is universally better

Would it be useful to switch on-the-fly? How to switch?

Solution: MAB (with UCB selection strategy)

MAB (Multi-Armed Bandit): maximize reward when playing over K machines in a casino (one machine at a time)
MAB tells the user when to switch between the machines, given:
Reward: evaluates the performance – the higher the better

In Kissat-MAB (Stable mode only):

Machines = {EVSIDS, CHB}
Decision point: restart
Play machine: use that heuristic for one restart period
Domain-specific reward: log₂(decisions) / distinctDecidedVars

More decisions with fewer decision variables 🡪 good locality 🡪 high reward
More decisions with more decision variables 🡪 poor locality 🡪 low reward

50

51 of 82

AE_kissat2025_MAB: SC’25 Winner�Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, Xinyun Wu: A Self-Optimizing Framework for SAT Solvers via Population Evolution and Large Language Model Collaboration. Proceedings of SAT Competition 2025.

Kissat 4.0.2 (Post-SC’24) + Kissat-MAB’s MAB heuristic for the Stable (SAT) stage with two upgrades:

New reward: log₂(decisions) / log₂(conflicts). Recall Kissat-MAB: log₂(decisions) / distinctDecidedVars

Favors satisfiable branches (good for the Stable stage)!
Undocumented, if suggested by a human or an LLM

LLM-suggested upgrade: momentum mechanism in MAB/UCB

Tracks recent performance of the chosen heuristic
Doing well (better than recent average) → stick with current choice
Doing poorly (worse than recent average) → more likely to switch

At SC’25, AE_kissat2025_MAB solved 10 more satisfiable instances than the next best solver!

The contribution of each of the two upgrade is unclear…

The first LLM-empowered SC winner … but likely not the last one! See:

Cunxi Yu, Rongjian Liang, Chia-Tung Ho, Haoxing Ren: Autonomous Code Evolution Meets NP-Completeness. arXiv:2509.07367, 2025.

51

52 of 82

Progress on SAT Competition Instances and Beyond

There is a significant progress in SAT on SC benchmarks

Progress ≈ Pareto optimization over the families or over {SAT,UNSAT}

Solve a certain family without a significant overhead on the rest

Non-trivial research & engineering task

Steadily expanding coverage across families 🡪 the progress is real!

Yet, many applications have additional requirements:

API extensions
Other (than SC) performance-oriented algorithms

52

53 of 82

Beyond SAT Competitions: Thoughts and Agenda

SAT API extensions:

Incremental SAT solving under assumptions is crucial (model checking, MaxSAT, planning, …)�Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT, 2003.
New & reviewed later: hooks into the SAT solver!

SC performance improvements do not always transfer to applications. Examples:

SAT-based circuit solution enumeration: IntelSAT outperforms CaDiCaL (except for dedicated UC-extraction queries)��Dror Fried, Alexander Nadel, Yogev Shalmon: AllSAT for Combinational Circuits. SAT 2023.

IntelSAT: designed for easy mostly satisfiable incremental queries, but significantly slower than CaDiCaL on SC instances

“Introducing Intel® SAT Solver” [video], MIAO Seminars

State-of-the-art anytime MaxSAT solvers use Glucose/IntelSAT

MaxSAT Evaluation 2021: Glucose-only SATLike-c won, while outperforming a version running Kissat for the 1^st query on 3/4 categories

IC3/PDR (model checking): Minisat outperforms CaDiCaL

New & reviewed later: GipSAT (dedicated IC3/PDR solver) is significantly faster than both Minisat & CaDiCaL��Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.

Further in focus: the promise (and delivery so far) of chronological backtracking for extensions and apps

53

54 of 82

Hooks into the SAT Solver: Bounded Path as a Motivating Example�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.

The problem: find an s🡪t path of a bounded (user-provided) cost on a grid

App @ Intel: clock routing in physical design
With holes & under constraints (design rules)

Without these, a heuristic approach would suffice

Can be easily translated into SAT

Constraints: connectivity & direction & bounded cost

Problem: plain SAT doesn’t scale

Fails even for shortest-path with no constraints on tiny 10×10 graphs!

Shortest-path is in P; bounded-path is NP-complete

Next: the 2 reasons for failure & solving them with hooks into SAT

Hooks: API extensions allowing external guidance

While still taking advantage of resoluting backtrack search

Clock routing solution @ Intel

With hooks: in production for over a decade; scales to industrial grids with millions of vertices
No hooks: 10×10 shortest-path failure

54

55 of 82

Bounded Path to SAT Problem: Heuristic Diverges�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.

55

s

t

Cost

Exceeded

Due to SAT solver’s locality principle, the next path will be very close!

56 of 82

56

s

t

Cost

Exceeded

Due to SAT solver’s locality principle, the next path will be very close!

Bounded Path to SAT Problem: Heuristic Diverges�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.

57 of 82

57

s

t

Cost

Exceeded

Due to SAT solver’s locality principle, the next path will be very close!

Solution:

Use a dedicated decision heuristic by hooking into SAT

The SAT solver asks the user for every decision (optional)

Sync by hooking into SAT’s backtrack and assignment events

The SAT solver notifies about every backtrack and assignment

Bounded Path to SAT Problem: Heuristic Diverges�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.

58 of 82

Applying Grid-Aware Heuristic Example�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.�

58

s

t

59 of 82

Bounded Path to SAT Problem: Self-Blocking�Amit Erez, Alexander Nadel: Finding Bounded Path in Graph using SMT for Automatic Clock Routing. CAV 2015.�

59

s

t

The problem:

The solver has blocked its own way 🡪 it’s stuck forever

Might happen even when a dedicated heuristic is used

Because of holes & constraints

Escaping via learning & blocking alone requires exponential #learnt-clauses

The solution:

Hooking: the high-level app adds a clause to escape when it identifies self-blocking

The user can ask the SAT solver to add a new clause

60 of 82

Hooks for All!�Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere: Satisfiability Modulo User Propagators. JAIR 2024.

A well-defined SAT API with hooks into the SAT solver (IPASIR-UP)

Implemented in the state-of-the-art solver CaDiCaL

Extends the applicability of SAT to the wide community!

No need to modify the SAT solver if you need to:

Add clauses on-the-fly
Implement and sync a custom decision heuristic

Successful examples from the paper:

Enumerating graphs within the SAT modulo Symmetries framework (SMS)
CaDiCaL outperformed Minisat and replaced it as the CDCL(T) engine in cvc5!

cvc5: leading SMT solver (widely used in verification)

60

61 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

61

62 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

62

X(v₁)

X(v₂)

X(v₃)

X(v₄)

X(v₅)

63 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

63

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 1

64 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

64

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 2

65 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

65

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 3

66 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS

SAT solvers are not reset between queries (activation variables reused)

66

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 4

67 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

IC3 (aka PDR) is a widely used complete model checking algorithm

Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011.

Incremental SAT-based: huge number of easy queries (SAT&UNSAT)

State-of-the-art implementations still use Minisat

The CAV’25 paper:

A dedicated SAT solver GipSAT
Main technique: filter out query-irrelevant variables

Exclude from VSIDS’s data structure
Remove clauses with query-irrelevant variables from watch lists

Other techniques:

A bucket-based data structure for VSIDS
SAT solvers are not reset between queries (activation variables reused)

67

68 of 82

Dedicated SAT Solving for IC3 (Model Checking)�Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang: Deeply Optimizing the SAT Solver for the IC3 Algorithm. CAV 2025.�

Domain-dedicated SAT solving works!

At least in the IC3 case…

68

69 of 82

Chronological Backtracking : Introduction�Alexander Nadel, Vadim Ryvchin: Chronological Backtracking. SAT 2018.��

CB always backtracks by one level

Not only when a unit clause is derived

69

z’@0

Propagated @ 0

A deep conflict yielding a unit clause

Non-Chronological Backtracking (NCB)

After Backtrack, Flip & BCP

Decision level 0

y

z’@0

Chronological Backtracking (CB)

Backtracks by 1 level 🡪 �tree retained!

Example:

z@0

x

a@5

z@0

x@5

a@5

Might propagate @ any level!

z still flipped @0

Propagation

y

z

Conflict! The conflict clause: (z’)

70 of 82

Chronological Backtracking in SAT�Alexander Nadel, Vadim Ryvchin: Chronological Backtracking. SAT 2018.�

Before 2018 (since Chaff): NCB considered an indisputable part of CDCL

2018: CB introduced in MapleLCMDistChronoBT

Challenging to implement: propagation doesn’t happen at last level only anymore

Main benefit in SAT: saves backtracking, reassignment & repropagation

Originally developed to solve a family of huge (>1,000,000,000 clauses) easily satisfiable instances

Eliminates repeated backtracking near satisfying assignments upon unit clause discovery

The trade-off: NCB-induced partial restarting and decision reordering can help locality

Surprisingly efficient in generic SAT solving: implementing CB in SC’17 winner won SC’18

Mixed heuristic: Backtrack <100 levels → NCB, else CB

Today: part of the leading SAT solvers

Yet, CB's impact on generic SAT solving is mild (likely due to the trade-off above)

70

71 of 82

The Promise of CB: SAT Applications & Extensions

CB promises to be game-changing whenever:

Systematic exploration of the space is required

Recently, delivered on the promise in enumeration and model counting

Giuseppe Spallitta, Roberto Sebastiani, Armin Biere: Disjoint projected enumeration for SAT and SMT without blocking clauses. AIJ 2025.

Mate Soos, Kuldeep S. Meel: Engineering an Efficient Probabilistic Exact Model Counter. CAV 2025.

Substantial performance impact on both domains!
… after overcoming non-trivial challenges, including:

Enumeration: generalization (aka implicant shrinking) without clauses
Model counting: eliminating double counting by additional logic

At least one of the following is costly: backtracking, assignment, propagation

Examples: Satisfiability Modulo Theories (SMT), AVATAR (first-order logic)
Benefit yet to be demonstrated: SMT assumes propagation @ the last level

CB and hooks into SAT:

SAT apps can benefit from CB. Recall the bounded-path example:
If your app requires CB, hook into CaDiCaL as it supports CB!

71

72 of 82

Recap

Introduced core SAT as resoluting backtrack search

BCP & 1UIP learning without implication graphs
Split on the way down, resolve on the way up

Reviewed recent developments in sequential SAT solving, including:

SAT Competition winners during 2021–2025, focusing on:

The LLM-empowered SC’25 winner AE-Kissat-MAB and its heuristic predecessors

Extensions & applications beyond SAT Competitions

Hooks into SAT for broader applicability (IPASIR-UP)
Domain-dedicated SAT solving for IC3 (GipSAT)
Chronological backtracking for extensions & apps: the promise and delivery so far

72

73 of 82

Backup

73

74 of 82

Kissat Variable Decision Heuristic�

Kissat has two search modes: Stable (SAT) and Focused (UNSAT)

Introduced in COMiniSatPS – the baseline of Maple series (SC’16—19 winners)�Chanseok Oh: Between SAT and UNSAT: The Fundamental Difference in CDCL SAT. SAT 2015: 307-323

Stable (SAT) mode uses EVSIDS with heap-based scores

EVSIDS �Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518

Bump when variable participates in conflict derivation: score[x] += increment
Increment grows exponentially: increment *= 1/0.95 ≈ 1.053 per conflict
All scores rescaled when any exceeds 10¹⁵⁰

Decision: pick variable with highest activity score

Focused (UNSAT) mode uses VMTF (Variable-Move-To-Front) with queue�Lawrence Ryan: Efficient algorithms for clause-learning SAT solvers. Masters thesis, Simon Fraser University, February 2004

Decision: pick most recently moved variable

74

75 of 82

CHB Decision Heuristic: Inspired by Reinforcement Learning�Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. AAAI 2016: 3434-3440�

Variable score Q(x) is maintained (the higher the better). Update:

Q(x) = (1 - α) × Q(x) + α × r(x)

When is Q(x) updated?

After every BCP, for all variables assigned at the current decision level

Reward function:

r(x) = mult / (#ConflictsNow - LastConflictTouching(x) + 1)

BCP led to a conflict 🡪 mult = 1.0 else mult = 0.9
α: Initial: 0.4; decays by 10⁻⁶ after each conflict; minimum: 0.06

Unlike EVSIDS, CHB updates each variable’s impact at assignment time

More responsively so in the beginning of the search (α: 0.4 → 0.06)

75

76 of 82

SAT Competition Winners (CNF & Appl. & Seq. & Non-incr. & All-inst.)

76

zChaff: 1UIP; BCP with 2WL; conflict-driven & local decision heuristic (VSIDS); restarts; clause deletion

Forklift: clause deletion with age&size; boost variable scores for all visited variables (conflict analysis)

Minisat: EVSIDS; conflict-clause-minimization; incremental SAT solving

SatELiteGTI: preprocessing (BVE, subsumption, self-subsumption) with gate identification

RSAT: phase saving

Precosat: luby restarts; additional preprocessing (failed literals & merging equivalent literals)

CryptoMiniSat: XOR clauses; on-the-fly subsumption

Core CDCL (RBS) Learning Decision/restart heuristics Clause management Pre/in-processing Mind pre-CNF Beyond Resolution Extensions

SAT Competition Winners (CNF & Appl. & Seq. & Non-incr. & All-inst.)

2002

zChaff

2003

Forklift

2004

zChaff

2005

SatELiteGTI

2006

2007

MiniSat

2008

Precosat

2009

2010

CryptoMiniSat

Moskewicz

Madigan

Zhao

Zhang

Malik

Goldberg

Novikov

Moskewicz

Madigan

Zhao

Zhang

Malik

Eén

Sörensson

Eén

Sörensson

Pipatsrisawat

Darwiche

Eén

Sörensson

Biere

Soos

MiniSat-based:

Armin Biere’s & derived:

Others:

RSAT

77 of 82

SAT Competition Winners (CNF & Appl. & Seq. & Non-incr. & All-inst.)

77

Glucose: literal block distance (LBD/glue) for clause quality; binary resolution during conflict analysis

Lingeling: elaborated in-processing

abcdSAT: Lingeling preprocessing (enhanced) & Glucose’s CDCL

MapleCOMSPS: SAT/UNSAT stages; 3-tiered clause management; LRB decision heuristic (SAT stage)

MapleLCMDist: DISTANCE heuristic (initially); vivification (made it work)

MapleLCMDistChronoBT: chronological backtracking

MapleLCMDistChronoBTDLv3: duplicate learnts 🡪 pervasive

Kissat: VMTF decision heuristic (UNSAT stage); advanced inprocessing; low-level optimizations (binaries inlined; watch arena); target-phase polarity selection with local search

Core CDCL (RBS) Learning Decision/restart heuristics Clause management Pre/in-processing Mind pre-CNF Beyond Resolution Extensions

2012

2013

2014

2015

2016

2017

2018

2019

2020

Glucose

Lingeling

Maple�COMSPS

Maple�LCMDist

Maple�LCMDist�ChronoBT

Maple�LCMDist�ChronoBTDLv3

Kissat

Audemard

Simon

Biere

Chen

Liang

Oh

Ganesh

Czarnecki

Poupart

Xiao

Luo

Li

Manya

Lu

Nadel

Ryvchin

Kochemazov

Zaikin

Kondratiev

Semenov

Biere

Fazekas

Fleury

Heisinger

abcdSAT

Glucose

Audemard

Simon

2011

MiniSat-based:

Armin Biere’s & derived:

Others:

78 of 82

SAT Competition Winners (CNF & Appl. & Seq. & Non-incr. & All-inst.)

78

Kissat-MAB: MAB heuristic to switch between EVSIDS and CHB (SAT mode)

Kissat-MAB-HyWalk: combining multiple local search strategies

SBVA-Cadical: made SBVA work

Kissat: clausal congruence closure; SBVA; dynamic glue limit; revisited vivification

AE-Kissat-MAB: reintroduced MAB heuristic in SAT mode with LLM-generated changes

Coming next:

Core CDCL (RBS) Learning Decision/restart heuristics Clause management Pre/in-processing Mind pre-CNF Beyond Resolution Extensions

2022

2023

2024

2025

Kissat-MAB

Cherif, Habet, Terrioux

2021

Kissat-MAB-HyWalk

Zheng, He, Chen, Zhou, Li

SBVA-Cadical

Haberlandt

Green

Kissat

Biere, Faller, Fazekas, Fleury, Froleyks, Pollitt

AE-Kissat-MAB

Ding, Luo,

C.M. Li, S. Li,

Chen,

Xiong, Wu

Kissat-MAB

AE-Kissat-MAB

SBVA

Clausal congruence closure

MiniSat-based:

Armin Biere’s & derived:

Others:

79 of 82

Clausal Congruence Closure�Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks: Clausal Congruence Closure. SAT 2024.

The idea: identify and solve Formal Equivalence Verification (FEV) between two circuits at CNF level

Previously: circuit-level solvers could quickly identify a miter & solve the problem, but SAT solvers failed

The technique: gradually extract gates

Requires careful implementation with gate normalization, especially when one of the circuits is optimized

Main result: clausal congruence closure is as good as circuit-level techniques!

Cheap enough to run till completion

79

UNSAT!

80 of 82

Bounded Variable Addition (BVA)�Norbert Manthey, Marijn J. H. Heule, Armin Biere: Automated Reencoding of Boolean Formulas. HVC 2012.��Andrew Haberlandt, Harrison Green, Marijn J. H. Heule: Effective Auxiliary Variables via Structured Reencoding. SAT 2023.��

de + abc

80

(d + a) (d + b) (d + c)

(e + a) (e + b) (e + c)

=

(x + a) (x + b) (x + c)

(x’ + d) (x’ + e)

BVA

BVA interpretation:

factorization (de is factor; abc is quotient): (d+a)(d+b)(d+c)(e+a)(e+b)(e+c) / de = abc
Re-encoding:

Implicit conversion to DNF, then encoding into a smaller CNF with an additional variable
Example, at-most-one(5) reencoding:

(d + a) (d + b) (d + c)

(e + a) (e + b) (e + c)

(d + e) (a + b)

(a + c) (a + d)

(x + a) (x + b) (x + c)

(x’ + d) (x’ + e)

BVA

(d + e) (a + b)

(a + c) (a + d)

Notes:

at-most-one(5) reencoding: any xy (not only de) can be factored out
BVA saves even more clauses when reencoding naïve encodings of at-most-one(k>5)

81 of 82

BVA Properties and History�Norbert Manthey, Marijn J. H. Heule, Armin Biere: Automated Reencoding of Boolean Formulas. HVC 2012.��Andrew Haberlandt, Harrison Green, Marijn J. H. Heule: Effective Auxiliary Variables via Structured Reencoding. SAT 2023.��

BVA Properties:

Always reduces #clauses
One of few SAT techniques beyond resolution (adds auxiliary variables)

BVA History:

Proposed in [MHB, HVC’12]
[HGH’23]: SBVA -- structured tie-breaking heuristic

Enabled winning SC’23 by SBVA-Cadical

Implemented in Kissat since the SC’24 winning version

Tie-breaking heuristic from [HGH’23] disabled

81

82 of 82

Chronological Backtracking : Introduction�Alexander Nadel, Vadim Ryvchin: Chronological Backtracking. SAT 2018.��

Chronological Backtracking: the Generic Algorithm

Given the conflict clause at level δ:

C=[c₁^@δ, c₂^@β<δ, c₃@^@≤β, …, c_i@^@≤β, …, c_|C|^@≤β]

Backtrack to δ-1, flip & propagate (BCP)

BCP level is clause-specific (the highest in the clause)!

NCB would backtrack to β and always propagate at β

82

z’@0

Propagated @ 0

A deep conflict yielding a unit clause

Non-Chronological Backtracking (NCB)

After Backtrack, Flip & BCP

Decision level 0

y

z’@0

Chronological Backtracking (CB)

Backtracks by 1 level 🡪 �tree retained!

Example:

z@0

x

a@5

z@0

x@5

a@5

Might propagate @ any level!

z still flipped @0

Propagation

y

z

Conflict! The conflict clause: (z’)