1 of 21

�Entailing Generalization Boosts Enumeration

Yogev Shalmon, Intel & The Open University of Israel

Dror Fried, The Open University of Israel

Alexander Nadel, Intel & Technion, Israel

Roberto Sebastiani, DISI University of Trento, Italy

SAT’24 Conference, Pune, India

August 21, 2024

1

2 of 21

Combinational Circuits

Gates correspond to logical operators (AND, OR)
Output depends solely on the inputs

In our context, only 1 output

No memory units (not sequential)

2

3 of 21

Satisfying a Combinational Circuit

3

4 of 21

Satisfying When Don’t-Cares are Around

4

5 of 21

Is Satisfaction Enough to Define a Solution?

5

No! Consider the following example:

6 of 21

Is Satisfaction Enough to Define a Solution?

6

7 of 21

Is Satisfaction Enough to Define a Solution?

7

8 of 21

Is Satisfaction Enough to Define a Solution?

8

9 of 21

Entailment Vs. Satisfaction�

9

[Sebastiani, arXiv’20], [MÖhle, Sebastiani, Biere, SAT’20]

10 of 21

What is Generalization?

10


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

11 of 21

What is Generalization?

11

Generalization


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

12 of 21

Our Observation: The Generalization Hierarchy

12

e-gen.

s-gen.

g-gen.

13 of 21

Entailing Generalization In Practice

13

14 of 21

Entailing Generalization: UC Generalization

14

15 of 21

Our Application: AllSAT Enumeration (AllSAT-CT)

15


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

Triggered by industrial application of Static Timing Analysis at Intel

16 of 21

Utilizing Entailing Generalization to Boost Enumeration

HALL - AllSAT enumeration tool for combinational circuits [Fried, Nadel, Shalmon, SAT’23]
HALL uses generalization-based blocking algorithms
We developed new algorithms that utilize entailing generalization (UC)
We integrated our algorithms into HALL

Main result: our algorithms boost the quality and the performance of HALL!

16

17 of 21

Experimental Results

Compared vs Hall (previous algorithms)
Compared vs dualiza (SAT & BDD modes)
In total, we tested 140 benchmarks (97 solved)
We evaluated:

Solved instances (Timeout of 3600s)
PAR-2 score (Run-time if solved; 2*Timeout if not solved)
Quality (The number of generated solutions, normalized to [0,1] - best/current)

Also, we experimented with different SAT solvers:

IntelSAT, CaDiCaL, MergeSat, CryptoMiniSAT

… and different algorithms:

Minimal/non-minimal UC, forward/backward simulation

17

18 of 21

Results

18

Algorithm	Description	PAR-2	Solved	Quality
ROC	s-gen. + e-gen.	24926.84	94	0.966
CORE	e-generalization	25938.17	94	0.888
CARMA		27073.55	94	0.886
HALL-TALE	s-generalization	92676.52	85	0.568
HALL-DUTY		99447.68	84	0.560
HALL-MARS		198771.01	70	0.412
dualiza_sat		263810.94	61	0.459
dualiza_bdd		332953.81	51	0.397

New

19 of 21

Quality Results: TALE vs CORE vs ROC

19

Comparing CORE vs TALE

Comparing ROC vs TALE

20 of 21

Conclusion & Future Work

20

21 of 21

Thank you for listening

Questions?