1 of 102

SAT Solving and Beyond: �A Fresh Intro and Recent Developments

Alexander Nadel

Technion, Data and Decision Sciences & NVIDIA, Israel

June 1, 2026

MIAO Online Seminar

This is an extended version of the talk “SAT Solving: A Fresh Intro and Recent Developments”, BIRS Seminar “Theory and Practice of SAT and Combinatorial Solving”, 2026

1

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 the talk “SAT Solving: A Fresh Intro and Recent Developments”, presented at BIRS Seminar “Theory and Practice of SAT and Combinatorial Solving”, 2026.

2 of 102

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:

Given a solution, it is aways easy to verify it.
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…

This intriguing gap between theory and practice makes SAT a fascinating problem!

2

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

clause #1

clause #2

Literals

3 of 102

Agenda

Core SAT as resoluting backtrack search

BCP & 1UIP learning without implication graphs

Briefly survey of SAT Competition winners till 2020
What’s new in (sequential) SAT solving:

Reviewing SAT Competition winners during 2021–2025
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

Beyond CNF reasoning: on generalizing solutions

The generalization hierarchy: CNF ≪ Circuit ≪ Dual Circuit

3

4 of 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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.
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 102

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

18 of 102

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a’

19 of 102

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

a’

b’

20 of 102

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 102

Core SAT as Resoluting Backtrack Search

a + b

b’ + c

b’ + c’

a’ + b

a + b

b’ + c

a’

b’

b

c’

22 of 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

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 102

1UIP Scheme

42 of 102

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 102

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 102

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 102

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 102

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 102

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 102

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

48

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

49 of 102

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

49

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:

50 of 102

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

50

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:

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:

Relevant Heuristics Review

51 of 102

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)

51

52 of 102

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

52

53 of 102

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 upgrades 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.

53

54 of 102

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

54

(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)

55 of 102

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

55

56 of 102

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

56

UNSAT!

57 of 102

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

Clausal congruence closure is a perfect example

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

57

58 of 102

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
Beyond CNF reasoning: on generalizing solutions

58

59 of 102

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

59

60 of 102

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

60

s

t

Cost

Exceeded

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

61 of 102

61

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.

62 of 102

62

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.

63 of 102

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

63

s

t

64 of 102

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

64

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

65 of 102

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)

65

66 of 102

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

67 of 102

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

X(v₁)

X(v₂)

X(v₃)

X(v₄)

X(v₅)

68 of 102

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)

68

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 1

69 of 102

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)

69

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 2

70 of 102

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)

70

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 3

71 of 102

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)

71

X(v₂)

X(v₄)

X(v₁)

X(v₃)

X(v₅)

Query 4

72 of 102

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)

72

73 of 102

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…

73

74 of 102

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

74

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’)

75 of 102

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

2001 (Chaff): NCB introduced along with 2WL-based BCP

Main benefit: locality -- NCB-induced partial restarting and decision reordering can be helpful
In hindsight: substantially simplified 2WL-based BCP implementation

2018 (MapleLCMDistChronoBT): CB reintroduced in a modern SAT solver

Main benefit: retains the trail; saves backtracking, reassignment & repropagation
We originally developed CB to solve a family of huge (>1,000,000,000 clauses) easily satisfiable instances

Eliminates repeated backtracking near satisfying assignments upon unit clause discovery

Challenging to implement under 2WL-based BCP: propagation doesn’t happen at last level only anymore

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 locality vs. retainment trade-off)

75

76 of 102

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:

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

76

77 of 102

On Generalizing Solutions: The Setting�Dror Fried, Alexander Nadel and Yogev Shalmon: AllSAT for Combinational Circuits. SAT 2023. �Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

Input: a solution S for a single-output combinational circuit

Solution: an assignment S to the inputs, s.t. the output is satisfiedby propagating S^**

Goal: generalize S

Replacing input values by X’s whenever possible, while ensuring S is still a solution
Generalization = prime implicant generation off a starting point

Explored since the 1950s�W. V. Quine. The problem of simplifying truth functions. The American Mathematical Monthly, 59(8):521–531, 1952. �E. J. McCluskey. Minimization of boolean functions. The Bell System Technical Journal, 35(6):1417–1444, 1956.

Extensive usage: IC3/PDR, Enumeration, Explainable AI, Symbolic Execution, …

** Solution definition will be refined later

78 of 102

Solution Example

1

0

1

79 of 102

Getting this Solution from SAT (via Tseitin Encoding)

1

0

1

(k + d + c')

(k' + d’)

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

(o)

80 of 102

Getting this Solution from SAT (via Tseitin Encoding)

1

0

1

(k + d + c')

(k' + d’)

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

(o)

81 of 102

Generalization @ CNF Level by Unassignment:�All Clauses Must be Satisfied, but One Literal is Sufficient

1

0

1

(k + d + c')

(k' + d’)

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

(o)

82 of 102

Generalization @ CNF Level by Unassignment:�All Clauses Must be Satisfied, but One Literal is Sufficient

X

1

0

1

(k + d + c')

(k' + d’)

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

(o)

83 of 102

Generalization @ CNF Level by Unassignment:�All Clauses Must be Satisfied, but One Literal is Sufficient

would’ve been unsatisfied: (m' + a + b)

X

1

0

1

(k + d + c')

(k' + d’)

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

would’ve been unsatisfied: (n' + c)

would’ve been unsatisfied: (n' + d)

(o)

84 of 102

Generalization @ CNF Level by Unassignment: Result

1

0

1

(k + d + c')

(k' + d')

(k' + c)

(m' + a + b)

(m + a')

(m + b')

(p' + k + n)

(p + k')

(p + n')

(o' + p + m)

(o + p')

(o + m')

(n + d' + c')

(n' + d)

(n' + c)

X

Can we do better?

Yes, but not @ CNF level!

(o)

85 of 102

Generalization by Forward Ternary Generalization:�Substitute the inputs by X one by one; stick if the output is still 1

1

0

1

X

86 of 102

Generalization by Forward Ternary Generalization:�Substitute the inputs by X one by one; stick if the output is still 1

1

0

1

X

(m' + a + b)

(m + a')

(m + b')

b:=X works @ circuit level (the output is still 1)
Doesn’t work @ CNF level (some of the clauses are not satisfied)

87 of 102

Generalization by Forward Ternary Generalization:�Substitute the inputs by X one by one; stick if the output is still 1

1

0

X

88 of 102

Generalization by Forward Ternary Generalization:�Substitute the inputs by X one by one; stick if the output is still 1

1

X

89 of 102

Generalization by Forward Ternary Generalization: Result

1

0

1

X

Can we do better still?

Yes, by defining solution by entailment rather than satisfaction!

Satisfaction: propagating the inputs renders o=1
Entailment: any substitution of input X’s to {0,1}’s propagates to o=1

Roberto Sebastiani: Are You Satisfied by This Partial Assignment? CoRR abs/2003.04225 (2020)

90 of 102

Generalization by Entailment �Solution: any substitution of X’s to {0,1}’s propagates to o=1

90

1

0

1

X

91 of 102

Generalization by Entailment�Solution: any substitution of X’s to {0,1}’s propagates to o=1

91

1

0

1

X

0

1

92 of 102

Generalization by Entailment: Result �Solution: any substitution of X’s to {0,1}’s propagates to o=1

92

1

0

1

X

0

1

X

93 of 102

The Generalization Hierarchy�Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

g: gate

s: satisfaction

e: entailment

94 of 102

The Generalization Hierarchy�Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

Every gate’s output isn’t X

Must hold to satisfy @ CNF level with Tseitin encoding
Algorithm:

Iteratively go over the clauses to make sure every C is satisfied by 1 literal only

1

0

1

X

95 of 102

The Generalization Hierarchy�Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

Propagating inputs 🡪 o:=1

Algorithm:

Forward/backward ternary simulation

1

0

1

X

Propagating inputs 🡪 o:=1

Algorithm:

Forward/backward ternary simulation

96 of 102

The Generalization Hierarchy�Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

Substituting all X’s by any {0,1}’s and propagating 🡪 o:=1

Algorithm:

Provide a SAT solver:

Dual (negated) circuit C'
the solution (over the inputs) as assumptions

The UNSAT core is the generalized solution!

1

0

1

X

0

1

X

97 of 102

The Generalization Hierarchy�Dror Fried, Alexander Nadel, Roberto Sebastiani and Yogev Shalmon: Entailing Generalization Boosts Enumeration. SAT 2024.

In practice, the following combination works best for circuit solution enumeration:

Forward ternary simulation, then minimal UNSAT core over the dual circuit!

Every gate’s output isn’t X

Must hold to satisfy @ CNF level with Tseitin encoding
Algorithm:

Iteratively go over the clauses to make sure every C is satisfied by 1 literal only

Propagating inputs 🡪 o:=1

Algorithm:

Forward/backward ternary simulation

J. Paul Roth, Willard G. Bouricius, and Peter R. Schneider. Programmed algorithms to

compute tests to detect and distinguish between failures in logic circuits. IEEE Trans. Electron.

Comput., 1967.

Substituting all X’s by any {0,1}’s and propagating 🡪 o:=1

Algorithm:

Provide a SAT solver:

Dual (negated) circuit C'
the solution S as assumptions

The UNSAT core is the generalized solution!

Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, and Ziv Nevo: Incremental formal verification of hardware. FMCAD, 2011.

98 of 102

Recap

Introduced core SAT as resoluting backtrack search

BCP & 1UIP learning without implication graphs

Split on the way down, resolve on the way up

Surveyed SAT Competition winners till 2020
Reviewed recent developments in sequential SAT solving, including:

SAT Competition winners during 2021–2025
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

The generalization hierarchy: CNF ≪ Circuit ≪ Dual Circuit

98

99 of 102

Backup

99

100 of 102

Preliminaries: Kissat’s 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
Locality principle: favors variables visited in recent conflicts

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

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

100

101 of 102

Preliminaries: CHB Decision Heuristic (ML-Inspired)�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)

CHB is the predecessor of LRB used in MapleCOMSPS (SC'16 winner)

101

102 of 102

SC’21 🡪 SC’25 MAB/UCB Adjustment Details

SC’21: UCB[i] = reward[i]/n[i] + √ (4 * log(N+1) / n[i])

reward[i] = accumulated reward for heuristic i
n[i] = number of times heuristic i was selected
N = total stable restarts
4 = exploration constant (fixed)

SC’25: UCB[i] = reward[i]/n[i] + √ (C_adaptive * log(N+1) / n[i])

C_adaptive = 4 / (momentum · (N+1))
momentum starts at 1.0, then adapts:

momentum *= 1.1 if current gain > recent average
momentum *= 0.9 if current gain < recent average

102