Introduction to SAT

Alexander Nadel

Technion, Data and Decision Sciences & Intel, Israel

Indian SAT+SMT School, 2024

August 18, 2024

Pune, Maharashtra, India

1

8/6/2024

​

​

PEG PDS DDI

Introduction

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

The original NP-Complete problem

• The famous Cook-Levin theorem (early 70s)

SAT has exponential complexity unless P = NP

P = NP (SAT): frequently called the most important outstanding question in CS

• If it is easy to check that a solution to a problem is correct, is it also easy to solve the problem?
• One of the 7 Clay Millennium Prize Problems – worth $1,000,000

2

8/6/2024

​

​

PEG PDS DDI

Introduction

SAT is an unresolved mystery!

Yet, SAT solvers are scalable widely used tools

Main goals for today:

• Explain how modern SAT solvers work
• Convey intuition why they work in practice
• Provide examples of applying SAT

​

3

8/6/2024

​

​

PEG PDS DDI

SAT Applications

4

8/6/2024

​

​

PEG PDS DDI

SAT Application Examples

5

8/6/2024

Optimization with

SAT@

​

​

PEG PDS DDI

SAT Resources

SAT Association: http://satassociation.org/

SAT Conferences: http://www.satisfiability.org/

SAT Competitions: http://www.satcompetition.org/

SATLive: http://www.satlive.org/

​

​

​

6

8/6/2024

​

​

PEG PDS DDI

Why am I Interested in SAT?

2002: stumbled upon SAT and completed my Master thesis about it (Hebrew University)

• Jerusat – won the Industrial, SAT category at SAT Competition 2004

2003: joined Intel

• Been developing & internally deploying SAT and SAT-based solvers (SMT, Model Checkers) ever since
• Till 2014: working on SAT-based validation as the rest of the semiconductor industry
• Since 2014: optimization (place & route, scheduling), test generation, physical design, lithography, …

2009: PhD about SAT (Tel-Aviv University)

2023: joined the Technion’s Data and Decision Sciences faculty as a part-time research fellow

• Looking for students!

Most SW is closed-sourced, but lately I was able to participate in some open-source projects:

• 2018: MapleLCMDistChronoBT SAT solver – won the SAT Competition 2018
• 2019–2024 : TT-Open-WBO-Inc MaxSAT solver – multiple medals in MaxSAT Evaluations
• 2022: Intel released my new SAT solver “Intel® SAT Solver” (IntelSAT), tuned for optimization flows

7

8/6/2024

​

​

PEG PDS DDI

Agenda

How does a conflict-driven SAT solver work?

• The core: backtrack search, Boolean Constraint Propagation (BCP), conflict analysis
• Follow the first SAT Competition winners (from Chaff till Minisat)

Applying SAT by example

• Paradigms: incremental SAT solving, SAT-based local search, example encodings
• Applications: Bounded Model Checking (BMC), proof-based abstraction refinement, bug hunting, anytime MaxSAT

Advanced core SAT algorithms

• Follow the SAT Competition winners after Minisat & discussion about incremental SAT

​

8

8/6/2024

​

​

PEG PDS DDI

Not in Today’s Agenda

SAT Solving

• Parallel SAT solving (divide & conquer, portfolio, cloud)
• Non-CNF formulas
• Deserves much more attention: inprocessing, encodings

SAT-based paradigms and solvers

• Satisfiability Modulo Theories (SMT)
• Quantified Boolean Formula (QBF)
• Model counting
• AllSAT – enumerating all solutions
• Model sampling

…

9

8/6/2024

​

​

PEG PDS DDI

SAT Fundamentals: Backtrack Search

The baseline algorithm in modern SAT solvers is backtrack search

Called DPLL or DLL

Davis, Martin; Logemann, George; Loveland, Donald: "A Machine Program for Theorem Proving". Communications of the ACM. 5 (7): 394–397. (1961). 

Davis, Martin; Putnam, Hilary: A computing procedure for quantification theory. Journal of the ACM 7 (1960)

​

​

10

8/6/2024

​

​

PEG PDS DDI

From Enumeration to DPLL

11

8/6/2024

Boolean Constraint Propagation (BCP): after a decision, apply the unit clause rule till fixed-point

0

1

0

Carry out backtrack search.

Stop when a model is found

0

The unassigned literal c₁ must be implied

a

b

c

Stop when a clause turns UNSAT

c₂

c₁

c₃

Falsified literal:

Satisfied literal:

Unassigned literal:

A unit clause -- one unassigned, rest falsified:

1

a

b

c

0

0

The unit clause rule: the unassigned literal in a unit clause must be 1

Implied in parent clause #1:

​

​

PEG PDS DDI

The Mystery of SAT Solver Scalability

DPLL: backtrack search with BCP until a model is found (SAT) or completion (UNSAT)

DPLL could handle formulas with <2,000 clauses

Modern SAT solvers cope with industrial instances of 100,000,000’s clauses

The introduction of Conflict-Driven-Clause-Learning (CDCL) or, simply, �Conflict-driven Solving was the birth of modern highly-scalable SAT solving

​

​

​

Learn from conflicts to drive & prune backtrack search

​

​

​

12

8/6/2024

​

​

PEG PDS DDI

CDCL: the Intuitive Principles

Learning and pruning

• Block already explored sub-spaces

Locality

• Focus the search on the relevant data
• Learn strong clauses from the local context

Well-engineered data structures

• Extremely fast Boolean Constraint Propagation (BCP)

Beyond CDCL

• Inprocessing
• Local search integration

​

​

13

8/6/2024

​

​

PEG PDS DDI

Basic CDCL Algorithm

Preprocess() // Simplify the formula

While (true)

• Literal l = Decide() // Choose the next literal to assign
• BCP(l) // Apply the unit clause rule till fixed point
• If (conflict)
• ConflictAnalysisLoop() // Learn a new conflict clause(s), backtrack and flip a variable
• If (learned an empty clause)
• Return UNSAT
• If (all the variables are assigned)
• Return SAT
• Occasionally, restart
• Occasionally, delete conflict clauses

14

8/6/2024

​

​

PEG PDS DDI

Conflict-driven SAT Solving: Seminal Work

15

8/6/2024

1996: GRASP by Joao P. Marques-Silva and Karem A. Sakallah

João P. Marques Silva, Karem A. Sakallah: GRASP - a new search algorithm for satisfiability. ICCAD 1996: 220-227��2001: Chaff by Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik

Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver. DAC 2001: 530-535

​

​

PEG PDS DDI

Chaff’s Conflict Analysis

16

8/6/2024

h@5(C₅)

b@2

c@3

d@4

e@5

f@5(C₆)

g@5(C₃)

a@1

Decision Level 4

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

Decision Level 1

Decision Level 2

Decision Level 3

Decision Level 5

Decision variable/literal

C₆= ¬e ∨ ¬h ∨ f

Implied literal

Conflict analysis starts

​

​

PEG PDS DDI

Implication Graphs and Conflict Analysis

Every vertex corresponds to an assigned literal

A decision literal has 0 incoming edges

A literal implied in clause C has |C|-1 incoming edges from every other literal in C

We only need the strongly connected component of the conflict

17

8/6/2024

h@5(C₅)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

a@1

b@2

c@3

d@4

e@5

g@5

¬ g@5

f@5

c@3

b@2

C₃

C₃

C₄

C₆

C₄

Implication graph

f@5(C₆)

C₆= ¬e ∨ ¬h ∨ f

h@5

C₅

C₆

g@5(C₃)

e@5

​

​

PEG PDS DDI

Implication Graphs and Conflict Analysis

Conflict cut

• Right (conflict): the two conflicting implications
• Left (reason): all the decision literals (roots)

Conflict clause

• Corresponds to every cut: includes one appearance of ¬l for every edge l🡪r in the cut
• Learning a conflict clause prevents the conflict from reappearing

18

8/6/2024

h@5(C₅)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

a@1

b@2

c@3

d@4

e@5

g@5

¬ g@5

f@5

c@3

b@2

C₃

C₃

C₄

C₆

C₄

Implication graph

f@5(C₆)

C₆= ¬e ∨ ¬h ∨ f

h@5

C₅

C₆

g@5(C₃)

e@5

¬f ∨ ¬c ∨ ¬b

¬h ∨ ¬e ∨ ¬c ∨ ¬b

¬e ∨ ¬c ∨ ¬b

​

​

PEG PDS DDI

Implication Graphs and Conflict Analysis

A UIP cut has exactly one literal l of the last level on the reason side of its edges

• l is a Unique Implication Point (UIP): a literal sufficient to imply the conflict at the last level
• A conflict clause is a UIP clause if it corresponds to a UIP cut

UIP’s are ordered starting from the conflict

19

8/6/2024

h@5(C₅)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

a@1

b@2

c@3

d@4

e@5

f@5(C₆)

C₆= ¬e ∨ ¬h ∨ f

g@5(C₃)

g@5

¬ g@5

f@5

c@3

b@2

C₃

C₃

C₄

C₆

C₄

h@5

C₅

e@5

¬f ∨ ¬c ∨ ¬b: 1UIP

¬h ∨ ¬e ∨ ¬c ∨ ¬b

¬e ∨ ¬c ∨ ¬b: 2UIP

C₆

Implication graph

​

​

PEG PDS DDI

Chaff’s Conflict Analysis

20

8/17/2024

h@5(C₅)

f@1(C₈)

c@3

¬f@3(C₇)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

a@1

b@2

c@3

d@4

e@5

g@5

¬ g@5

f@5

e@5

c@3

b@2

1UIP

C₇ = ¬f ∨ ¬c ∨ ¬b

a@1

b@2

C₃

C₃

C₄

C₆

C₄

g@3

¬ g@3

a@1

¬ f@3

C₁

C₁

C₂

C₂

1UIP

C₈ = f ∨ ¬a

a@1

c@3

b@2

• Learn a falsified asserting clause C=[c₁^@δ, c₂^@β<δ , c₃^@≤β , … , c_|C|^{@≤ β}]
• 1UIP clause: fewest variables out of all UIP clauses (UIP clauses have one variable @ δ)
• Backtrack to level β: called Non-Chronological Backtracking (NCB) 🡪 C becomes unit
• Flip & imply c₁ in its parent C and run BCP

NCB to 3

NCB to 1

Implication graph

f@5(C₆)

g@3(C₁)

C₆= ¬e ∨ ¬h ∨ f

h@5

C₅

C₆

g@5(C₃)

¬c@2

¬b@3

¬e@4

d@5

g@6

h@7

C₇

C₇

Conflict analysis completed

​

​

PEG PDS DDI

GRASP’s Conflict Analysis

b@2

a@1

g@3

a@1

b@2

c@3

d@4

e@5

f@5(C₅)

g@5

¬g@5

f@5

e@5

c@3

1UIP

C₆ = ¬f ∨ ¬c ∨ ¬b

C₃

C₃

C₄

C₅

C₄

2UIP 🡪 1UIP

C₇ = ¬e ∨ f

¬f@3(C₆)

a@1

b@2

c@3

d@4

f@1(C₈)

a@1

¬f@3

C₁

C₁

C₂

C₂

1UIP

c@3

b@2

2UIP🡪1UIP

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ f

b@2

C₉ = ¬c ∨ ¬b ∨ ¬f

C₈ = f ∨ ¬a

• Backtrack to the conflict level δ: called NCB in GRASP (unnamed today)
• Learn a falsified asserting 1UIP clause C=[c₁^@δ, c₂^@β<δ , c₃^@≤β , … , c_|C|^{@≤ β}]
• Learn a clause per every other UIP of the last level
• Backtrack to level δ-1: called Chronological Backtracking (CB) today.
• Flip & imply c₁ in its parent C and run BCP

CB to 4

¬g@3

Backtrack to conflict level 3

CB to 2

In GRASP, f is a special kind of a “flipped” decision variable at level 5, but GRASP learns as if ¬f were implied at level 3

g@5(C₃)

g@3(C₁)

¬g@1(C₄)

¬c@1(C₃)

d@3

¬e@4

Conflict analysis completed

​

​

PEG PDS DDI

Up-to-date Conflict Analysis Algorithm �Covers GRASP & Chaff & Modern Solvers

1. Backtrack before conflict analysis: backtrack to the conflict level δ, if required
• Required in GRASP
• Not required in Chaff: current decision level ≡ conflict level
2. Learn an asserting clause C=[c₁^@δ, c₂^@β<δ, c₃@^@≤β, …, c_i@^@≤β, …, c_|C|^@≤β]
• 1UIP clause in both GRASP & Chaff
• Return UNSAT, if the clause is empty
3. Optionally, learn other clauses
• GRASP: a clause for every other UIP of the conflict decision level
4. Backtrack: backtrack to a level in [β, β+1, …, δ-1] -- renders the asserting clause unit
• GRASP -- always δ-1: Chronological Backtracking (CB) in today’s terminology
• Chaff -- always β: Non-Chronological Backtracking (NCB) in today’s terminology
5. Flip c₁ by implying it in C and run BCP

22

8/6/2024

​

​

PEG PDS DDI

Boolean Constraint Propagation (BCP) Essentials

BCP is carried out after every decision and flip and consumes 80-90% run-time

What?

• Identify and propagate in unit clauses (performance)

​

​

• Identify and report any conflicts (correctness)

​

How?

• Visit a clause when one of its watched literals is falsified
• Every literal l holds a Watch List (WL) with all the clauses where l is watched

23

8/6/2024

Falsified literal:

Satisfied literal:

Unassigned literal:

​

​

PEG PDS DDI

Efficient Data Structure for BCP

• GRASP watched all the literals in every clause
• It is sufficient to watch two non-falsified literals: SATO’s Head/Tail!
• Watching: visiting during BCP

Hantao Zhang: SATO: An Efficient Propositional Prover. CADE 1997: 272-275

• Chaff’s 2WL: watching the first two literals – no need to visit during backtracking!

​

• as long as: decision-level(falsified watch) ≥ decision-level(falsified non-watch)
• Caching one literal inside the watches & inlining binary clauses

Sörensson, N., Eén, N.: MiniSAT 2.1 and MiniSAT++ 1.0 - SAT race Editions. SAT, Competitive Event Booklet (2008) (caching one literal)� Geoffrey Chu, Aaron Harwood, Peter J. Stuckey: Cache Conscious Data Structures for Boolean Satisfiability Solvers. J. Satisf. Boolean Model. Comput. 6(1-3): 99-120 (2009) (caching one literal & inlining binary clauses)

8/6/2024

c₄

c₅

c₇

c₂

c₁

c₃

c₆

Falsified literal:

Satisfied literal:

Unassigned literal:

Unknown literal:

Non-falsified literal:

Non-satisfied literal:

c₄

c₅

c₇

c₃

c₂

c₆

c₁

​

​

PEG PDS DDI

BCP assuming NCB

For every satisfied literal l in the literal stack Π (literals to be propagated)

• For <h ≠ ¬l ∈ C, C> ∈ WL(¬l) h: cached literal; C: the visited clause, where c₁≡¬l or c₂≡¬l
• If h is satisfied: continue C is satisfied: no conflict, C isn’t unit 🡪 skip C

Clause visit: assume WLOG c₂ ≡ ¬l

• If c₁ is satisfied: continue
• If a non-falsified k ≠ c₁∈C exists
• Swap(C, k, ¬l)
• Remove <h ≠ ¬l ∈ C, C> from WL(¬l)
• Add <h’ ≠ k ∈ C, C> to WL(k) h’: heuristical
• Else (unit or falsified)
• If c₁ is unassigned, imply c₁ and add c₁ to Π (unit)

​

• If c₁ is falsified, report a conflict and return C (falsified)

25

8/6/2024

Falsified literal:

Satisfied literal:

Unassigned literal:

Unknown literal:

Non-falsified literal:

Non-satisfied literal:

​

​

PEG PDS DDI

Agenda

How does a conflict-driven SAT solver work?

• The core: backtrack search, Boolean Constraint Propagation (BCP), conflict analysis
• Follow the first SAT Competition winners (from Chaff till Minisat)

Applying SAT by example

• Paradigms: incremental SAT solving, SAT-based local search, example encodings
• Applications: Bounded Model Checking (BMC), proof-based abstraction refinement, bug hunting, anytime MaxSAT

Advanced core SAT algorithms

• Follow the SAT Competition winners after Minisat & discussion about incremental SAT

​

​

26

8/6/2024

​

​

PEG PDS DDI

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

27

2002

zChaff

2003

Forklift

2004

zChaff

2005

SatELiteGTI

2006

RSAT

2007

MiniSat

MiniSat

2008

Precosat

2009

2010

CryptoMiniSat

2011

Glucose

2012

2013

2014

2015

2016

2017

2018

2019

2020

2021

Glucose

Lingeling

Lingeling

abcdSAT

Maple�COMSPS

Maple�LCMDist

Maple�LCMDist�ChronoBT

Maple�LCMDist�ChronoBTDLv3

Kissat

KissatMAB

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

Audemard

Simon

Audemard

Simon

Biere

Biere

Chen

Liang

Oh

Ganesh

Czarnecki

Poupart

Xiao

Luo

Li

Manya

Lu

Nadel

Ryvchin

Kochemazov

Zaikin

Kondratiev

Semenov

Biere

Fazekas

Fleury

Heisinger

Cherif

Habet

Terrioux

2022

2023

KissatMAB-HyWalk

Zheng

He�Chen

Zhou

Li

SBVA-CaDiCaL

Haberlandt

Green

​

​

PEG PDS DDI

Chaff

Covered:

• Conflict analysis
• BCP

To cover:

• Variable State Independent Decaying Sum (VSIDS) decision heuristic
• The first conflict-driven decision heuristic
• Conflict clause deletion
• Restarts

28

8/6/2024

​

​

PEG PDS DDI

Variable State Independent Decaying Sum (VSIDS)

Each literal l has a counter S(l), initialized to 0

For every new clause C=[c₁, c₂, …, c_n], S(c_i) is incremented for every c_i∈C

Including initial and conflict clauses

The (unassigned) variable and polarity with the highest counter is chosen

Ties are broken randomly

Periodically (once in 256 conflicts), all the counters are halved.

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 0

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 0

Count literal appearances in the initial formula

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 0

Pick a literal with maximal score

¬e🡪{h,i}

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 0

¬e🡪{h,i}

¬a🡪{d}

Pick an unassigned literal with maximal score

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 0

¬e🡪{h,i}

Conflict

¬a🡪{d}

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 1

¬h ∨ a ∨ c ∨ ¬b ∨ k

Increment scores for conflict clause literals

¬e🡪{h,i}

¬a🡪{d}

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 256

Assume the threshold of 256 is reached

¬e🡪{h,i}

¬a🡪{d}

​

​

PEG PDS DDI

VSIDS Example

Heuristic-related data

Search tree

Conflicts till now: 256

Halve the scores

¬e🡪{h,i}

¬a🡪{d}

​

​

PEG PDS DDI

VSIDS vs. Static Heuristics

Pre-Chaff static heuristics

• Go over all clauses that are not satisfied
• Compute some function f(a) for each literal—based on frequency
• Choose literal with maximal f(a)

VSIDS was a breakthrough

• Extremely low overhead
• Conflict-driven 🡪 dynamic and local
• Based on recent conflicts
• Focuses the search to learn from the local context

​

​

PEG PDS DDI

Conflict Clause Deletion

Maintaining too many clauses slows down the solver

D. Gelperin: Deletion-directed search in resolution-based proof procedures, in Proc. of the 3rd Int. Joint Conf. on Artificial Intelligence (1973), pp. 47–50.

Chaff’s strategy:

• Mark a clause for deletion, once 100-200 literals become unassigned

39

8/6/2024

​

​

PEG PDS DDI

Restarts

C. P. Gomes, B. Selman and H. A. Kautz: Boosting combinatorial search through randomization, in Proc. of AAAI (1998), pp. 431–437

Refocus the search by starting from important variables

Chaff: restart every 700 conflicts

40

8/6/2024

​

​

PEG PDS DDI

Chaff

Preprocess()

While (true)

• Literal l = Decide() // VSIDS
• BCP(l) // 2WL
• If (conflict)
• ConflictAnalysisLoop() // 1UIP + non-chronological backtracking
• If (learned an empty clause)
• Return UNSAT
• If (all the variables are assigned)
• Return SAT
• Occasionally, restart // Every 700 conflicts
• Occasionally, delete conflict clauses // Mark for deletion, when 100-200 lit’s are unassigned

41

8/6/2024

​

​

PEG PDS DDI

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

42

2002

zChaff

2003

Forklift

2004

zChaff

2005

SatELiteGTI

2006

RSAT

2007

MiniSat

MiniSat

2008

Precosat

2009

2010

CryptoMiniSat

2011

Glucose

2012

2013

2014

2015

2016

2017

2018

2019

2020

2021

Glucose

Lingeling

Lingeling

Maple�COMSPS

Maple�LCMDist

Maple�LCMDist�ChronoBT

Maple�LCMDist�ChronoBTDLv3

Kissat

KissatMAB

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

Audemard

Simon

Audemard

Simon

Biere

Biere

Chen

Liang

Oh

Ganesh

Czarnecki

Poupart

Xiao

Luo

Li

Manya

Lu

Nadel

Ryvchin

Kochemazov

Zaikin

Kondratiev

Semenov

Biere

Fazekas

Fleury

Heisinger

Cherif

Habet

Terrioux

MiniSat-based:

​

Armin Biere’s& derived:

Others:

2022

2023

KissatMAB-HyWalk

SBVA-CaDiCaL

Haberlandt

Green

Zheng

He�Chen

Zhou

Li

abcdSAT

​

​

PEG PDS DDI

BerkMin & Forklift by Goldberg & Novikov

Forklift: industrial closed-source solver (Cadence)

We discuss Forklift’s direct ancestor BerkMin (won Handmade, SAT category at SC’02)

Goldberg, Novikov: BerkMin: A fast and robust SAT-solver, DATE, 2002.

Clause deletion is based on “age” and size. The strategy, simplified:

• Age: remove clauses which did not participate in recent conflict clause derivation
• Size: keep short clauses forever (|C|<8)

Restarts every 550 conflicts

Innovation in decision heuristics

• Boost the score for all the literals visited during conflict analysis (rather than only in the conflict clause)
• Used in modern solvers
• Clause-based heuristic

​

43

8/6/2024

​

​

PEG PDS DDI

Extended Score Boost Example

44

8/6/2024

h@5(C₅)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ h

a@1

b@2

c@3

d@4

e@5

g@5

¬ g@5

f@5

c@3

b@2

C₃

C₃

C₄

C₆

C₄

Implication graph

f@5(C₆)

C₆= ¬e ∨ ¬h ∨ f

h@5

C₅

C₆

g@5(C₃)

e@5

¬e ∨ ¬c ∨ ¬b

• Chaff’s: boost the scores of ¬e, ¬c and ¬b
• BerkMin: additionally to ¬e, ¬c and ¬b, boost the scores of h, f, g, ¬g

​

​

PEG PDS DDI

BerkMin & Forklift by Goldberg & Novikov

Forklift: industrial closed-source solver (Cadence)

We discuss Forklift’s direct ancestor BerkMin (won Handmade, SAT category at SC’02)

Goldberg, Novikov: BerkMin: A fast and robust SAT-solver, DATE, 2002.

Clause deletion is based on “age” and size. The strategy, simplified:

• Age: remove clauses which did not participate in recent conflict clause derivation
• Size: keep short clauses forever (|C|<8)

Restarts every 550 conflicts

Innovation in decision heuristics

• Boost the score for all the literals visited during conflict analysis (rather than only in the conflict clause)
• Used in modern solvers
• Clause-based heuristic

​

45

8/6/2024

​

​

PEG PDS DDI

Clause-based Heuristics

Berkmin

• The conflict clauses are placed on a stack
• The next variable is picked from the topmost unsatisfied clause
• If no such clause exists, use VSIDS

HaifaSAT (3^d in three Industrial categories at SC’05)

Roman Gershman, Ofer Strichman: HaifaSat: A New Robust SAT Solver. Haifa Verification Conference 2005: 76-89

• Move clauses visited during conflict analysis to the top

CBH -- Eureka SAT solver (2^nd at SR’06)

Nachum Dershowitz, Ziyad Hanna, Alexander Nadel: A Clause-Based Heuristic for SAT Solvers. SAT 2005: 46-60

• Either all the clauses (including the initial clauses) or only the initial clauses are on the stack
• Move clauses visited during conflict analysis to the top

Added value w.r.t variable-based heuristics: picks interrelated variables

Didn’t make it to mainstream modern solvers, though CBH is occasionally very useful in my experience

• 2023: modified CBH works great for constraint-based product configuration ��Matthias Gorenflo, Tomás Balyo, Markus Iser, Tobias Ostertag: Decision Heuristics in a Constraint-based Product Configurator. ConfWS 2023: 51-59

​

​

​

​

46

8/6/2024

​

​

PEG PDS DDI

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

47

2002

zChaff

2003

Forklift

2004

zChaff

2005

SatELiteGTI

Armin Biere’s& derived:

2006

RSAT

2007

MiniSat

MiniSat

2008

Precosat

2009

2010

CryptoMiniSat

2011

Glucose

2012

2013

2014

2015

2016

2017

2018

2019

2020

2021

Glucose

Lingeling

Lingeling

Maple�COMSPS

Maple�LCMDist

Maple�LCMDist�ChronoBT

Maple�LCMDist�ChronoBTDLv3

Kissat

KissatMAB

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

Audemard

Simon

Audemard

Simon

Biere

Biere

Chen

Liang

Oh

Ganesh

Czarnecki

Poupart

Xiao

Luo

Li

Manya

Lu

Nadel

Ryvchin

Kochemazov

Zaikin

Kondratiev

Semenov

Biere

Fazekas

Fleury

Heisinger

Cherif

Habet

Terrioux

MiniSat-based:

Others:

2022

2023

KissatMAB-HyWalk

SBVA-CaDiCaL

Haberlandt

Green

abcdSAT

Zheng

He�Chen

Zhou

Li

​

​

PEG PDS DDI

MiniSat & SatELite: Seminal Works

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

• Minisat solver
• “Test of time” award at SAT’22
• Simple & elegant engineering: the ancestor of a long line of solvers!
• Impactful heuristics & algorithms:
• Exponential VSIDS (EVSIDS)
• sometimes still called VSIDS today
• Conflict clause minimization
• Incremental-under-assumptions API: enabler of major real-world flows

Niklas Eén, Armin Biere: Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75

• SatELite Preprocessing

�

48

8/6/2024

​

​

PEG PDS DDI

Minisat’s Decision Heuristic

Separate variable and polarity heuristics

• Keep score per variable, rather than per literal
• Choose 0 as the first polarity

EVSIDS

• Increment activity by an exponentially increasing increment (g=1/f)^#conflict
• Minisat: f=0.95 🡪 g≈1.05
• Rescale when activity (for any variable) becomes higher than 10¹⁰⁰
• g *= 10^-100
• #conflict = 1
• Even more dynamic than VSIDS

Both features (further updated) made it to today’s state-of-the-art solvers

​

49

8/6/2024

​

​

PEG PDS DDI

Restart & Clause Deletion in Minisat

Restarts

• Geometric series
• starting from 100, with the factor of 1.5
• Too slow: didn’t make it to modern solvers

Clause deletion

• Activity-based: smoothing BerkMin’s scheme
• Each clause is associated with a float activity
• Each time a clause is used in conflict analysis, its activity is increased
• Periodically, the less active clauses are deleted (half of the clauses)
• Still in use (along with other ideas)�

50

8/6/2024

​

​

PEG PDS DDI

MiniSat & SatELite: Seminal Works

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

• Minisat solver
• Simple & elegant engineering: the ancestor of a long line of solvers!
• Impactful heuristics & algorithms:
• Exponential VSIDS (EVSIDS)
• sometimes still called VSIDS today
• Conflict clause minimization
• Incremental-under-assumptions API: enabler of major real-world flows
• “Test of time” award at SAT’22

Niklas Eén, Armin Biere: Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75

• SatELite Preprocessing

�

51

8/6/2024

Next: after some preliminary material

After presenting SatELite

​

​

PEG PDS DDI

Resolution and Variable Elimination

52

8/6/2024

C ∨ l

D ∨ ¬l

​

Resolution (Davis & Putnam’60)

C ∨ D

a ∨ b ∨ l

c ∨ b ∨ ¬l

a ∨ b ∨ c

l is the pivot

Variable Elimination by Resolution (Davis & Putnam’60)

C₁ ∨ l

D₁ ∨ ¬l

C₂ ∨ l

D₂ ∨ ¬l

…

C_n ∨ l

D_m ∨ ¬l

C₁ ∨ D₁

C₁ ∨ D₂

…

C₁ ∨ D_m

…

C₂ ∨ D₁

C₂ ∨ D₂

…

C₂ ∨ D_m

​

…

C_n ∨ D₁

C_n ∨ D₂

…

C_n ∨ D_m

a ∨ b ∨ l

d ∨ l

c ∨ b ∨ ¬l

¬c ∨ ¬ b ∨ ¬l

​

a ∨ b ∨ c

c ∨ b ∨ d

¬c ∨ ¬ b ∨ d

Equisatisfiable

​

​

PEG PDS DDI

Subsumption and Self-Subsuming Resolution

53

8/6/2024

Subsumption

C

C ∨ D

​

C

C ∨ D

​

a ∨ b

a ∨ b ∨ c

​

a ∨ b

a ∨ b ∨ c

​

C ∨ D ∨ l

C ∨ ¬l

​

Self-subsuming Resolution

C ∨ D ∨ l

C ∨ ¬l

​

a ∨ b ∨ l

b ∨ ¬l

a ∨ b

b ∨ ¬l

​

​

PEG PDS DDI

SatELite Preprocessor

Run the following till fixed-point

• Variable elimination
• Bounded: the number of clauses doesn’t grow�or grows by a constant factor
• Gate identification: next slide
• Subsumption for removing subsumed clauses:

​

​

​

• Self-subsuming resolution for removing literals:

Crucial on many difficult instances ever since 2005!

54

8/6/2024

a ∨ b ∨ l

d ∨ l

c ∨ b ∨ ¬l

¬c ∨ ¬ b ∨ ¬l

​

a ∨ b ∨ c

c ∨ b ∨ d

¬c ∨ ¬ b ∨ d

a ∨ b

a ∨ b ∨ c

​

a ∨ b

a ∨ b ∨ c

​

a ∨ b ∨ l

b ∨ ¬l

a ∨ b

b ∨ ¬l

​

​

PEG PDS DDI

SatELite with Gate Identification

Idea: reduce the number of generated resolvents when eliminating a variable

How (on an AND-gate example; applicable to other gates too):

• Assume the algorithm considers eliminating the variable g
• Was g created by translating an AND-gate to clauses?
• Are the following clauses (or their simplified variants) present:
• Negative 🡪 optimization can’t be applied. Positive:
• Let the gate definition clauses be G = G⁺ ∪ G^- and the rest be R = R⁺ ∪ R^-
• + clauses contain g; - clauses contain ¬g
• Create only the resolvents between G and R!
• Resolving between G⁺ and G^- yield tautologies
• Resolving between R⁺ and R^- is unnecessary 🡪 next slide

55

8/6/2024

G⁺

G^-

​

​

PEG PDS DDI

SatELite with Gate Identification: Cont.

Resolving between R⁺ and R^- is unnecessary: the resolvents are obsolete

​

​

It can be yielded solely by resolutions between G and R:

56

8/6/2024

P ∨ a

P ∨ g

N ∨ ¬g

¬g ∨ a

g ∨ ¬a ∨ ¬b

¬g ∨ b

R⁺

R^-

G^-

G⁺

N ∨ ¬a ∨ ¬b

P ∨ b

P ∨ N ∨ ¬b

P ∨ N

​

​

PEG PDS DDI

(Learned Clause) Minimization

The idea:

• During conflict analysis,
• given a learnt clause C,
• remove unnecessary literals from C by resolution with parent clauses

Local minimization

Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22 (2004)

Recursive minimization

Niklas Sörensson, Armin Biere: Minimizing Learned Clauses. SAT 2009: 237-243

• In MiniSat since 2005
• Standard nowadays, applied for every learnt clause

57

8/6/2024

​

​

PEG PDS DDI

Local Minimization�

58

8/6/2024

C₁= ¬a ∨ b

C₂= ¬b ∨ c

C₃= ¬b ∨ ¬c ∨ ¬d ∨ e

C₄= ¬b ∨ ¬c ∨ ¬d ∨ ¬e

a@1

b@1

1UIP

C₅ = ¬b ∨ ¬c ∨ ¬d

c@1

d@2

e@2

¬ e@2

a@1

b@1

c@1

d@2

C₆ = ¬b ∨ ¬d

• Given a newly learnt clause C, remove literals, whose antecedents (in the implication graph) are already in C
• By applying self-subsuming resolution with the parent clause

e@2

​

​

PEG PDS DDI

Local Minimization Shortcoming�

d@2

e@2

C₁= ¬a ∨ b

C₂= ¬a ∨ ¬b ∨ c

C₃= ¬a ∨ ¬c ∨ ¬d ∨ e

C₄= ¬a ∨ ¬c ∨ ¬d ∨ ¬e

a@1

b@1

1UIP

C₅ = ¬a ∨ ¬c ∨ ¬d

c@1

d@2

e@2

¬ e@2

a@1

b@1

c@1

C₆ = ¬a ∨ ¬b ∨ ¬d

A new literal 🡪 local minimization fails

However, a further resolution step with C₁ would have yielded C₇ = ¬a ∨ ¬d, which subsumes C₅

• Given a newly learnt clause C, remove literals, whose antecedents (in the implication graph) are already in C
• By applying self-subsuming resolution with the parent clause

​

​

PEG PDS DDI

Recursive Minimization�

60

8/6/2024

C₁= ¬a ∨ b

C₂= ¬a ∨ ¬b ∨ c

C₃= ¬a ∨ ¬c ∨ ¬d ∨ e

C₄= ¬a ∨ ¬c ∨ ¬d ∨ ¬e

a@1

b@1

1UIP

C₅ = ¬a ∨ ¬c ∨ ¬d

c@1

d@2

e@2

¬ e@2

a@1

b@1

c@1

d@2

• Given newly a learnt clause C, try to remove literals one-by-one in decreasing assignment order by continuous resolution with the parents till either:
• A new level or a new decision variable is reached 🡪 removal not possible
• Literals already in the clause reached 🡪 remove the literal from the clause

C₆ = ¬a ∨ ¬b ∨ ¬d

C₇ = ¬a ∨ ¬d

e@2

​

​

PEG PDS DDI

MiniSat in Non-Incremental Mode

Preprocess() // Variable elimination with gate identification & subsumption & self-subsuming resolution

While (true)

• Literal l = Decide() // Variable-based EVSIDS + polarity 0
• BCP(l)
• If (conflict)
• ConflictAnalysisLoop() // minimized 1UIP
• If (learned an empty clause)
• Return UNSAT
• If (all the variables are assigned)
• Return SAT
• Occasionally, restart // geometric series
• Occasionally, delete conflict clauses // activity-based

61

8/6/2024

​

​

PEG PDS DDI

Agenda

How does a conflict-driven SAT solver work?

• The core: backtrack search, Boolean Constraint Propagation (BCP), conflict analysis
• Follow the first SAT Competition winners (from Chaff till Minisat)

Applying SAT by example

• Paradigms: incremental SAT solving, SAT-based local search, example encodings
• Applications: Bounded Model Checking (BMC), proof-based abstraction refinement, bug hunting, anytime MaxSAT

Advanced core SAT algorithms

• Follow the SAT Competition winners after Minisat & discussion about incremental SAT

​

​

​

62

8/6/2024

​

​

PEG PDS DDI

Hardware Circuit Example

63

8/6/2024

definitions:

​

I(C₀) := FALSE;

I(C₁) := FALSE;

X(C₀) := C₀ ⊕ en;

X(C₁) := C₁ ⊕ (C₀ ∧ en);

​

constraints:

​

en 🡪 ¬X(en)

​

​

2-Bit Counter, counting when en=1

​

​

PEG PDS DDI

Hardware Model Checking

Model Checking: given a circuit and a property, does the property always hold?

• Safety property: something bad will never happen
• Example: the counter never reaches the value 11

64

8/6/2024

definitions:

​

I(C₀) := FALSE;

I(C₁) := FALSE;

X(C₀) := C₀ ⊕ en;

X(C₁) := C₁ ⊕ (C₀ ∧ en);

​

constraints:

​

en 🡪 ¬X(en)

​

proof obligations:

​

¬(C₀ ∧ C₁)

​

2-Bit Counter, counting when en=1

​

​

PEG PDS DDI

Hardware Model Checking

Model Checking: given a circuit and a property, does the property always hold?

• Safety property: something bad will never happen
• Example: the counter never reaches the value 11

65

8/6/2024

definitions:

​

I(C₀) := FALSE;

I(C₁) := FALSE;

X(C₀) := C₀ ⊕ en;

X(C₁) := C₁ ⊕ (C₀ ∧ en);

​

constraints:

​

en 🡪 ¬X(en)

​

proof obligations:

​

¬(C₀ ∧ C₁)

​

2-Bit Counter, counting when en=1

​

​

PEG PDS DDI

Bounded Model Checking (BMC)

BMC: given a circuit ϕ and a property P, verify P until a user-given bound n

​

​

​

​

​

​

​

​

• For every bound b∈{1,…,n}
• The property holds at bound b iff (ϕ unrolled to bound b) ∧ ¬P is UNSAT
• If it’s SAT, the model comprises the trace of a bug

66

8/6/2024

​

​

PEG PDS DDI

BMC Example

The property: h🡪b

​

​

PEG PDS DDI

BMC Example: Cycle 0

a

b

h

g

c₀

A user-given initial value

The property: h🡪b

​

​

PEG PDS DDI

BMC Example: Cycle 0

a

b

h

g

c₀

h ∨ ¬g ∨ ¬c₀

¬h ∨ g

¬h ∨ c₀

g ∨ ¬a ∨ ¬b

¬g ∨ a

¬g ∨ b

¬b

h

​

The negation of the property h🡪b:

UNSAT: the property holds!

The property: h🡪b

​

​

PEG PDS DDI

BMC Example: Cycle 1

a

b

h

g

c₀

b_x

h_x

c_x

a_x

g_x

The property: h🡪b

​

​

PEG PDS DDI

BMC Example: Cycle 1

a

b

h

g

c₀

h ∨ ¬g ∨ ¬c₀

¬h ∨ g

¬h ∨ c₀

g ∨ ¬a ∨ ¬b

¬g ∨ a

¬g ∨ b

¬b_x

h_x

​

The negation of the property h_x🡪b_x:

b_x

h_x

c_x

c_x ∨ ¬h

¬c_x ∨ h

a_x

g_x

g_x ∨ ¬a_x ∨ ¬b_x

¬g_x ∨ a_x

¬g_x ∨ b_x

h_x ∨ ¬g_x ∨ ¬c_x

¬h_x ∨ g_x

¬h_x ∨ c_x

UNSAT!

The property: h🡪b

​

​

PEG PDS DDI

Re-Using Relevant Information from Previous Cycles

G₀ and G₁: hold globally

T₀ and T₁: hold temporary

• solely for a particular cycle

72

The property: h🡪b

​

​

PEG PDS DDI

Pervasive Clause Learning (GRASP)

Cycle 0: create a SAT instance G₀ ∧ T₀ and solve it

• Let G₀^* be the set of pervasive conflict clauses, that is conflict clauses that depend only on G₀

Cycle 1: create a SAT instance G₀ ∧ G₀^* ∧ G₁ ∧ S₁ and solve it

73

a ∨ ¬h

g

G₀^*

T₀

T₁

​

​

PEG PDS DDI

Incremental SAT Solving under Assumptions (Minisat)

Cycle 0: create a SAT instance and solve it under the temporary assumptions T₀

• T₀ clauses are not part of the instance, instead:
• The literals of T₀ are used as the first decision, or assumptions
• Any learnt clause which depends on an assumption a, will contain a itself or derived literals 🡪 all the learnts are pervasive!
• If one of the assumptions must be flipped, the solvers returns UNSAT

Cycle 1: add the clauses C₁ to the same SAT instance and solve under the assumptions T₁

74

a ∨ ¬h

Assumptions

Assumptions

T₀

T₁

​

​

PEG PDS DDI

Incremental SAT Solving under Assumptions

Basic API:

• AddClause(Clause C)
• Solve(Literals A)

Output:

• SAT iff F ∧ A is SAT
• F: all the clauses added so far
• A: current assumptions

Allows the user to add groups of clauses temporarily (for invocation #i)

• Using a new selector (activation) variable s
• To add a temporary clause T_i: AddClause(T_i ∨ s)
• Solve(A ∧ ¬s)
• To delete all the temporary clauses afterwards: do nothing or add a unit clause s

​

75

​

​

PEG PDS DDI

Incremental SAT Solving under Assumptions

A breakthrough

• Extremely easy to use
• Very efficient, since it retains the following info across all the queries:
• the conflict clauses
• heuristical data: variable scores, clause activities, …

Incremental solving under assumptions is widely used, including:

• Hardware & Software Validation
• SAT-based Optimization, including MaxSAT

My personal industrial experience: can’t recall any non-incremental SAT application

Minisat: SatELite preprocessing is incompatible with incremental solving

• Later works make it compatible:�

Alexander Nadel, Vadim Ryvchin, Ofer Strichman: Preprocessing in Incremental SAT. SAT 2012: 256-269

Katalin Fazekas, Armin Biere, Christoph Scholl: Incremental Inprocessing in SAT Solving. SAT 2019: 136-154

76

8/6/2024

​

​

PEG PDS DDI

Unsatisfiable Core in Terms of Assumptions

Extended API:

• AddClause(Clause C)
• Solve(Literals A)
• If UNSAT:
• Is assumption l∈A required for unsatisfiability proof?

Algorithm outline

• Conflict at decision level 0: unrelated to the assumptions
• None of the assumptions is required
• Otherwise, an assumption must have been flipped
• Go over the trail backwards
• Mark all the decision variables (must be assumptions!), connected to the flipped assumption
• Return the marked assumptions

​

​

​

77

8/6/2024

​

​

PEG PDS DDI

78

8/6/2024

seen: marks variables connected to the flipped assumption

p: the flipped assumption

out_conflict: the returned set of assumptions in the core

Go over the trail backwards

A decision variable: must be an assumption, since the flip must have occurred at an assumption level

An implied variable: mark all the variables in its parent

​

​

PEG PDS DDI

Proof-based Abstraction Refinement Example

The unsatisfiable core in terms of the latches is required

No Bug

Valid

Model Check A

BMC(M,P,k)

Cex C at unrolling depth k

Bug

No

A 🡨 A ∪ latches in the UNSAT core of BMC(M,P,k)

Inputs: model M, property P �Output: does P hold under M?

Abstract model A 🡨 { }

Spurious?

Yes

Cut latches into free inputs

Kenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17

Aarti Gupta, Malay K. Ganai, Zijiang Yang, Pranav Ashar: Iterative Abstraction using SAT-based BMC with Proof Analysis. ICCAD 2003: 416-423

​

​

PEG PDS DDI

SAT-based Local Search: �Finding a Solution Near an Assignment

Find a solution near an assignment M={v₁=σ₁, v₂=σ₂, …, v_n=σ_n}

Polarity-based

​

• Change only the polarity selection heuristic
• Whenever a decision variable v_i is chosen, choose σ_i as its first polarity

80

8/6/2024

�Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel:�SAT-based semiformal verification of hardware. FMCAD 2010: 25-32

​

​

PEG PDS DDI

Original Application: Bug Hunting

New Initial �states

New Initial �states

New Initial �states

initial

states

deep bugs

Max BMC

Bound

Needed to generate diverse solutions on the boundary!

​

​

PEG PDS DDI

Original Application: DiverseKSet for Bug Hunting

DiversekSet in SAT: generate a user-given number of diverse solutions

• Maximize the average Hamming distance between the solutions

Diverse solutions, given an empty CNF

• 000000
• Any model
• 111111
• Flip every variable
• 001110
• Pick a random value
• 110001
• Balance the values for every variable

Given a CNF formula:

• SAT-based local search: fix the polarities to match the current target solution (which would maximize the Hamming distance)
• Run SAT incrementally
• Adjust the target solution

​

82

8/6/2024

​

​

PEG PDS DDI

Optimization in SAT

OptSAT(F, ψ): given a propositional formula F in CNF and a Pseudo-Boolean objective function ψ, return a model to F which minimizes ψ

• A Pseudo-Boolean (PB) function: a mapping from every full assignment to a real number

​

​

83

8/6/2024

Example: F = (a + b) (a + ¬c) (¬a + c)

H has 3 models:

• M₁={a=0, b=1, c=0}
• M₂={a=1, b=0, c=1}
• M₃={a=1, b=1, c=1}

​

​

PEG PDS DDI