Conflict-driven SAT Solving

Alexander Nadel, Intel Israel

“25 years of SAT“ Session @ SAT’22 Conference

August 4, 2022

Technion, Haifa, Israel

1

​

​

PEG PDS DDI

1/11

The Scalability of SAT is Phenomenal

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

• Although, SAT complexity is exponential, unless P=NP

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

​

​

PEG PDS DDI

2/11

Agenda

Today’s focus: in-depth dive into the “core of the core”

• Conflict analysis loop
• Boolean Constraint Propagation (BCP)

Not covered today

• Conflict-driven heuristics: decision, restart, clause deletion, …
• Enhanced learning: minimization, on-the-fly subsumption, …

​

​

PEG PDS DDI

3/11

Conflict-driven SAT Solving: Seminal Work

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

4/11

Boolean Constraint Propagation (BCP) Essentials

BCP consumes 80-90% of SAT run-time

What?

• Identify and propagate in unit clauses (performance)

​

​

• Identify and report any conflicts (correctness)

​

How?

• Every literal l holds a Watch List -- WL(l) with all the clauses where l is watched
• When literal l is falsified, visit all the clauses in WL(¬l)

Falsified literal:

Satisfied literal:

Unassigned literal:

​

​

PEG PDS DDI

5/11

Efficient Data Structure for BCP

• GRASP watched all the literals
• 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

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)

7/28/2022

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

6/11

Conflict Analysis Loop in Chaff

Right-hand side: the conflict

Left-hand side: the reason, including the rightmost Unique Implication Point (UIP) of the last level

f@5(C₅)

Decision Level 4

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 ∨ f

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 in Chaff
• Backtrack to level β: called Non-Chronological Backtracking (NCB) in Chaff 🡪 C becomes unit
• Flip & imply c₁ in its parent C and run BCP

NCB to 3

NCB to 1

Decision Level 1

Decision Level 2

Decision Level 3

Decision Level 5

Decision variable/literal

Implication graph

g@5(C₃)

g@3(C₁)

​

​

PEG PDS DDI

7/11

Conflict Analysis Loop in GRASP

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

C₇ = ¬e ∨ ¬c ∨ ¬b

¬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

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ f

b@2

C₉ = ¬c ∨ ¬b ∨ ¬a

C₈ = f ∨ ¬a

• Backtrack to the conflict level δ: called NCB in GRASP
• 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) in later literature!
• 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₁)

​

​

PEG PDS DDI

8/11

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

1. Backtrack before conflict analysis: backtrack to the conflict level δ, if required
• Required in GRASP and called Non-Chronological Backtracking (NCB) 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
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] -- makes 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

​

​

PEG PDS DDI

9/11

Conflict Analysis Loop Evolvement

Maple_LCM_Dist_ChronoBT (MapleCB): the return of Chronological Backtracking (CB)

Alexander Nadel, Vadim Ryvchin: Chronological Backtracking. SAT 2018: 111-121

• A backtracking heuristic choosing between CB and NCB
• Today: Maple-based solvers, Cryptominisat, Kissat alter between CB and NCB
• CB algorithm is similar to GRASP’s
• Integrating CB with post-GRASP BCP data structures turned out to be highly non-trivial
• Because of simultaneous propagation at several levels
• BCP must be adjusted to prevent correctness & performance issues
• Useful BCP invariants are still violated

Cadical’19: custom (score-based) backtracking

Sibylle Möhle, Armin Biere: Backing Backtracking. SAT 2019: 250-266

• Backtrack to the decision level with the highest variable score
• Applied by Cadical & IntelSAT

CB & BCP integration: implemented, but not discussed

​

1996

GRASP

2001

Chaff

2018

Maple_LCM_Dist_ChronoBT

2019

Cadical’19

Chaff’s alg. (one 1UIP cls. & NCB) is the state-of-the-art

​

​

PEG PDS DDI

10/11

Integrating CB and BCP

Example of a necessary adjustment

• ¬c₁ and ¬c₂ are assigned @1 < max_level(C)
• Can’t happen with NCB, where the assigned level is always ≥ max_level(C)
• Must swap lit’s & update WL’s to watch two highest falsified lit’s
• Essential for correctness – in order not to miss conflicts after backtracking!

Useful invariants are still violated even with the adjustments:

• lowest implication: no assigned literal can be implied at a lower level
• lowest conflict: every conflict, BCP returns a clause �falsified at the lowest possible level

Intel® SAT Solver (IntelSAT): a new formally proven BCP alg. with a possible solution

Alexander Nadel: Introducing Intel® SAT Solver. SAT 2022.

There is more to it! Looking forward to the next 25 years!

​

​

Falsified literal:

Unassigned literal:

@10

@20

@10

Satisfied literal:

​

​

PEG PDS DDI

11/11