Solving Huge Instances with Intel® SAT Solver

Alexander Nadel, Intel and Technion, Israel

SAT 2023, Alghero, Italy

July 7, 2023

1

7/2/2023

​

​

PEG PDS DDI

The Paper in a Nutshell

Goal: enable solving huge instances with billions of clauses using a CDCL SAT solver

The SAT solver: “Intel® SAT Solver” (IntelSAT); the 2023 release is called IS23

• Core idea: IS23 can store clauses compressedly using fewer than 32 bits per literal
• All the CDCL algorithms work with the compressed clause data structure underneath
• Compression is optional (compile-time) and largely transparent to solver developer

Main empirical result – there are gigantic instances only IS23 can solve

Variable succession matters for efficient compression

• Variable succession: the order in which variables are provided to the solver

2

7/2/2023

​

​

PEG PDS DDI

Literal Representation in SAT

Consider a variable v_i

• i is the order (aka succession), in which the user provides variables to the solver

A literal l∈{v_i, ¬v_i} is represented by its literal index li(l). In most solvers:

• li(v_i) = 2i
• li(¬v_i) = 2i + 1

3

7/2/2023

​

​

PEG PDS DDI

Clause Management in SAT

Long (>2 literals) clauses are stored in the clause buffer

Layout of an initial clause:

• Learnt clauses have extra-fields

Example: C₁=(v₁ ∨ v₂ ∨ ¬v₃) ∧ C₂=(¬v₁ ∨ v₂ ∨ v₃)

​

​

Each clause C is uniquely identified by its clause index ci(C) – index in the buffer

In our example: ci(C₁) = 0; ci(C₂) = 4

​

​

4

7/2/2023

This row contains #bits

​

​

PEG PDS DDI

Limitation when Solving Huge Instances: Clause-Index Width�

Most solvers have a 32-bit clause-index

• Minisat, Glucose, Maple-based solvers (e.g., MergeSAT), Kissat, default CryptoMiniSat, IntelSAT

For huge instances, 32-bit indexing is not sufficient, since 2³² space is exhausted

The following solvers support 64-bit clause-index

• CryptoMiniSat can be compiled in 64-bit mode (since May 2017)
• CaDiCaL is natively 64-bit based

64-bit support lifts the indexing limitation, but inflates the memory usage

• Data structures pointing to clauses become twice as big
• Excessive memory usage becomes the limiting factor, when the input CNF is huge

5

7/2/2023

​

​

PEG PDS DDI

Clause Compression: Core Idea

Literal-width lw(clause C) is the minimal #bits, required to store C’s literals

Compression: store every clause C using lw(C) bits per literal

Example: C₁=(v₁ ∨ v₂ ∨ ¬v₃) ∧ C₂=(¬v₁ ∨ v₂ ∨ v₃)

Standard:

​

Compressed (lw(C₁) = lw(C₂)= 3):

​

​

6

7/2/2023

6×3=18 bits overall < one 32-bit word

8×32=256 bits overall

​

​

PEG PDS DDI

Clause Compression in IS23

Clauses are stored in multiple bit-arrays (clause buffers)

Given a clause C, its bit-array is uniquely determined by C’s 11-bit hash value hash(C):

• Literal-width lw(C): 5 bits
• Clause-size-width: 5 bits
• Learnt-status: 1 bit

hash(C) is calculated at creation time

• Rarely, hash(C) may change (e.g., when C is simplified), in which case C is moved to another bit-array

Bit-arrays are stored in a hash table

• Given hash(C), one can access C’s bit-array

7

7/2/2023

​

​

PEG PDS DDI

Compressed Clause-Index

C’s compressed clause-index (64 bits overall) stores hash(C) and the actual index:

​

​

​

Clause-index contains all the necessary information to access and parse C

• C’s hash to fetch C’s bit-array
• The bit where C starts in its bit-array
• Literal-width, clause-size-width and learnt-status to parse C

​

8

7/2/2023

​

​

PEG PDS DDI

IS23’s (the 2023 Release of IntelSAT) API

Templated C++ API (parameter values are chosen by the user at compile-time):

IS23<clause-index-width=32, literal-index-width=32, is-compressed=0>

• Under some constraints, detailed in the paper

Instantiations, studied in this paper:

• <32,32,0>: default
• <64,32,0>: 64-bit clause-index
• <64,32,1>: 64-bit clause-index & clause compression

​

​

​

9

7/2/2023

​

​

PEG PDS DDI

Experimental Set-up: S(n) -- Trivially SAT Instances

U(n): trivially unsatisfiable family with n var’s & 2ⁿ clauses in every instance

• Every clause contains all the n variables
• All the clauses are different
• U(2) = (¬v₁∨ ¬v₂) ∧ (¬v₁∨ v₂) ∧ (v₁∨ ¬v₂) ∧ (v₁∨ v₂)

S(n): trivially satisfiable family with n+1 var’s & 2ⁿ clauses in every instance

• S(n) is created from U(n) by adding a new variable v_n+1 to every clause
• S(2) = (¬v₁∨ ¬v₂ ∨ v₃) ∧ (¬v₁∨ v₂ ∨ v₃) ∧ (v₁∨ ¬v₂ ∨ v₃) ∧ (v₁∨ v₂ ∨ v₃)

What is the largest n for which S(n) is solvable?

Machines: 790Mb of memory, no timeout, no memory limit

​

10

7/2/2023

​

​

PEG PDS DDI

Experimental Results over S(n) instances

Only the compressed IntelSAT IS23-64C can solve S(33)

IS23-64C consumes ~half the memory of IS23-64 / CaDiCaL

• Memory consumption in IS23-64C is dominated by the Watch Lists – the next candidate for compression

​

11

7/2/2023

64-bit CryptoMiniSat

32-bit IntelSAT

64-bit IntelSAT

64-bit IntelSAT with compression

2³³ = 8,589,934,592 clauses and 2³³ ×(33+1) = 292,057,776,128 literals overall

​

​

PEG PDS DDI

Experimental Set-up: Finding One Placement

Application: cell placement – a critical stage in chip design

• Placing cells (rectangles) on a grid under optimization requirements

Our SAT-based anytime placement optimization flow is productized @ Intel

• Aviad Cohen, Alexander Nadel and Vadim Ryvchin, “Local Search with a SAT Oracle for Combinatorial Optimization” [presentation: pptx (with narration), pdf]. TACAS’21.

The empirical challenge which triggered this work:

• Some instances were too large for finding even the initial solution

Generated publicly available P(R) family

• Placing R rectangles of random width&height in [1-10] on a 10³×10³ grid

Timeout: 48 hours

Memory limit: 512Gb

12

7/2/2023

​

​

PEG PDS DDI

Experimental Results: Finding One Placement

Only IS23-64 solved P(5000) with almost 1B variables and 4.3B clauses

CaDiCaL solved only P(3000) being 4.8X slower and using 2.5X more memory

IS23-64C vs. IS23-64

• IS23-64C was usually slower than IS23-64 (unless it had fewer conflicts)
• because of overhead of bitwise operations when accessing clauses, but
• the margin was surprisingly low
• IS23-64C used only slightly less memory than IS23-64: compressed the clauses by ~1.5X, but memory consumption was dominated by other factors

13

7/2/2023

Finding one placement. The first three columns provide the number of rectangles (in hundreds), variables in CNF (in millions) and clauses in CNF (in millions). Each subsequent pair or triplet of columns corresponds to one solver. Each shows, for the corresponding solver, either: (1) the run-time (in hours), the memory usage (in GB) and, optionally, the number of conflicts (in thousands), or (2) the reason for a failure.

​

​

PEG PDS DDI

Experimental Set-up: Finding Many Placements

A flavor of the placement problem: find many (1,000,000) placements

• So that one could select promising placements as starting point for optimization

Implemented the basic blocking AllSAT algorithm (in IntelSAT and CaDiCaL and used an existing CryptoMiniSat implementation)

• Find a placement (SAT solution)
• Block it using a blocking clause over the important variables
• Important variables represent the bottom-left coordinate of every cell (rectangle)
• Repeat till reaching the user-given solution threshold

Two IS23-64C versions for testing variable succession:

• IS23-64CL: important variables are the lowest (first) in the variable succession
• IS23-64CH: important variables are the highest (last) in the variable succession

Compared with the 3 state-of-the-art AllSAT Toda tools -- {bc,nbc,bdd}_minisat_all

Timeout & memory limit: 10 hours & 32Gb

​

14

7/2/2023

​

​

PEG PDS DDI

Experimental Results: Finding 1,000,000 Placements

Only IS23-64CL was able to find all the solutions for P(900) and P(1000)

This time, IS23-64CL used significantly less memory than IS23-64

IS23-64CL solved 2 more instances than IS23-64CH: variable succession matters!

External solvers, including the AllSAT Toda tools, weren’t competitive

15

7/2/2023

Finding 10⁶ placements. The first column in both the sub-tables shows the number of rectangles (in hundreds); the upper table also contains two columns with the number of variables and clauses in CNF (in millions). Each subsequent triplet of columns shows, for one solver: the number of solutions (in thousands), the run-time (in hours) and the memory usage (in GB); in case of a failure, the last two columns per solver show its reason instead.

​

​

PEG PDS DDI

Conclusion & Future Work

Solved giganitic instances with billions of clauses using IS23 -- the 2023 version of IntelSAT:

• Trivially satisfiable: >8,500,000,000 clauses
• Find a placement: >4,300,000,000 clauses
• Find 1,000,000 placements: >170,000,000 clause

Core idea: store clauses compressedly using fewer than 32 bits per literal

Dedicated variable succession scheme enabled solving larger AllSAT placement instances

Future work:

• Explore other applications minding the variable succession
• Can different literal widths be useful
• 64 bits: to support gigantic instances with billions of variables
• 16 bits: to save memory for small instances
• Compress the Watch Lists

16

7/2/2023

​

​

PEG PDS DDI

Backup

17

7/2/2023

​

​

PEG PDS DDI

IS23’s (the 2023 Release of IntelSAT) API

Templated C++ API (parameters are chosen by the user at compile-time):

IS23<clause-index-width=32, literal-index-width=32, is-compressed=0>

• Constraint: 8 ≤ literal-index-width ≤ clause-index-width ≤ K
• For a K-bit operating system

Instantiations, studied in this paper:

• <32,32,0>: default
• <64,32,0>: 64-bit clause-index
• <64,32,1>: 64-bit clause-index & clause compression

Literal-index-width can be customized too (it’s 32 bits for every modern solver)

• <64, 64, 1>: for gigantic instances with billions of variables
• <32, 16, 0>: 16-bit literals to save memory for small instances

​

​

​

​

18

7/2/2023

​

​

PEG PDS DDI

Clause Compression Discussion

Compression’s impact on performance

• On one hand, compression might deteriorate the performance
• Bitwise operations are required to access literals
• On the other hand, compressed storage may result in fewer cache misses

How to design the compressed buffer?

• The following data must be available for parsing a clause:
• Literal-width (to parse individual literals)
• Clause-size-width (to store and access the clause size)
• Learnt or initial (to know whether there are additional fields in the clause)

Storing a fixed amount of additional bits per clause would be wasteful in terms of both

• Memory (additional bits), and
• Performance (additional bitwise operations per clause)

​

19

7/2/2023

​

​

PEG PDS DDI

Compressed Clause-Index

C’s compressed clause-index (64 bits overall) stores hash(C) and the actual index:

​

​

​

Clause-index contains all the necessary information to access and parse C

• C’s hash to fetch C’s bit-array
• The bit where C starts in its bit-array
• Literal-width, clause-size-width and learnt-status to parse C

To save bits, we store the compressed size |C|* instead of the actual size |C| in the clause

• Clause-size-width in hash(C) is determined, based on |C|*

​

20

7/2/2023

​

​

PEG PDS DDI

Clause-Size-Width and Compressed Size |C|* per |C|

21

7/2/2023

​

​

PEG PDS DDI

Compressed Clause-Index

C’s compressed clause-index (64 bits overall) stores hash(C) and the actual index:

​

​

​

Clause-index contains all the necessary information to access and parse C

• C’s hash to fetch C’s bit-array
• The bit where C starts in its bit-array
• Literal-width, clause-size-width and learnt-status to parse C

Clause-size-width sw(C) and the clause-size value in C are optimized for space

• sw(C)=0 for |C|=3-clauses (size not stored for them at all!); sw(C)=1 for |C|=4-clauses, etc.

​

22

7/2/2023

​

​

PEG PDS DDI

Clause Compression: Example

23

7/2/2023

​

​

PEG PDS DDI

Variable Succession

Variable succession: the order in which the user creates variables

Variable succession has a vital impact on literal-width, and thus on the quality of memory compression

Example: swapping v₃ and v₆ (G 🡪 G’) saves 6 bits overall

• C₁: highest index 13 🡪 7, thus lw 4🡪3, hence |C₁|*(4-3)=3 bits are saved
• C₂: highest index 12 🡪 7, thus lw 4🡪3, hence |C₂|*(4-3)=3 bits are saved
• C₃: highest index 5 🡪 6, thus lw 3🡪3, hence no changes in the number of bits

​

​

24

7/2/2023

​

​

PEG PDS DDI

Variable Succession is Expected to Matter in Practice: Examples

1. Selector variables
• Added by the users to groups of clauses to enable turning groups on/off with assumptions
• Typically appear last in the variable succession (created after the input problem is translated to CNF)
• Having selectors first is expected to have a substantial impact on the literal-width, thus the memory consumption & potentially the run-time
• Not tested in the paper
2. Important variables in blocking clauses in AllSAT (enumeration)
• Blocking AllSAT for finding N solutions distinct in important variables:
• Find a solution using incremental SAT
• Block it with a clause over the important variables
• All the blocking clauses consist only of the important variables
• Placing the important variables first in the succession substantially compresses the blocking clauses
• Enables solving larger instances for the industrial problem of finding many placements!

We propose that the user determines variable succession upfront. Automation would not be trivial.

25

7/2/2023

​

​

PEG PDS DDI

Agenda

Clause Buffer Data Structure and its Limitations for Huge Instances

The API of IS23 -- the 2023 Version of IntelSAT

Clause Compression

Variable Succession

Experimental Results

Conclusion & Future Work

26

7/2/2023

​

​

PEG PDS DDI

Variable Succession

Variable succession: the order in which the user creates variables

Variable succession has an immediate impact on

• literal-widths of clauses, and thus
• the quality of memory compression

Speculative example:

• Selector variables are used to mark groups of clauses to be able to turn groups on/off with assumptions
• Typically appear last in the variable succession
• Having selectors first is expected to have a substantial impact on the literal-width

Example empirically verified in the paper: important variables in blocking AllSAT

​

27

7/2/2023

​

​

PEG PDS DDI

Intel SAT® Solver (IntelSAT) Review

Alexander Nadel, “Introducing Intel® SAT Solver”. SAT’22 [long presentation (presented at MIAO Seminar on Feb. 28, 2023), MIAO Seminar video]

Full-fledged CDCL solver

Tuned for solving rapid, incremental, mostly satisfiable queries

• Useful for anytime optimization (anytime MaxSAT in the paper)

Used 32-bit clause-index

​

28

7/2/2023

I

​

​

PEG PDS DDI

Literal Representation in SAT

Consider a literal l=v_i or l=¬v_i

• i is the order (aka succession), in which the user provides variables to the solver

l is represented by its literal index li(l). In most solvers:

• li(v_i) = 2i
• li(¬v_i) = 2i + 1

Examples:

• li(v₂) = 4
• li(¬v₂) = 5
• li(v₇) = 14
• li(¬v₇) = 15

​

29

7/2/2023

​

​

PEG PDS DDI

Application: cell placement – a critical stage in chip design�

30

7/2/2023

0

8

8

The grid where to place the cells

The cells to be placed

c₁

c₂

c₃

c₄

c₅

0

8

8

Cell Placement w/o Optimization: Output

• The cells are placed
• Already NP-complete!

Basic input:

​

​

PEG PDS DDI