Enumerating All Boolean Matches

1

​

​

What is Boolean Matching?

• Given two circuits, are they equivalent?

​

2

​

​

What is Boolean Matching?

3

0

​

​

What is Boolean Matching?

• Given two circuits, are they matching (under permutation)?

​

​

4

​

​

What is Boolean Matching?

5

​

​

Our Motivation

6

​

​

Our Context

7

​

​

Previous Work - BooM

• BooM: the only Boolean matching approach for enumerating all matches
• We build upon BooM’s algorithm: the sifter – BooMS

​

• BooMS uses two buckets (SAT Instances):
• All Mappings – initialized with all the permutations (matches + mismatches)
• Mismatches – initialized with only the mismatches
• BooMS iteratively removes mismatches from “All Mappings” to get the matches
• Each time, getting the next mismatch from the “Mismatches” bucket

8

[Lai, Jiang, Wang, ICCAD’10], [Lai, Jiang, Wang, DAC’10]

​

​

BooMS in High Level

9

SAT instance

​

​

BooMS in High Level

10

SAT instance

mismatch

​

​

BooMS in High Level

11

SAT instance

Generalization

multiple mismatches

mismatch

​

​

BooMS in High Level

12

SAT instance

Generalization

Block Mismatches

mismatch

multiple mismatches

​

​

BooMS in High Level

13

SAT instance

All Matches!

No more mismatches!

​

​

BooMS in High Level

14

SAT instance

All Matches!

Enumerate all matches

​

​

BooMS Limitations

The strength on BooMS lays in blocking multiple mismatches together

However:

• Still needs to enumerate all the matches one-by-one
• Generalization for NP-Equivalence is “outdated”
• No generalization for P-Equivalence (with a good reason)

​

​

15

​

​

Our Contributions

• Two new algorithms:
• New picker algorithm EBatP that captures & block many matches at once
• New “sift-and-pick” algorithm EBatC combining BooMS + EBatP
• Better generalization for P- and NP-Equivalence:
• Using new generalization techniques for NP-Equivalence
• Brand new generalization for P-Equivalence
• Novel mismatch-blocking for P-Equivalence
• Open-source tool EBat, solves 3-4x more instances than BooMS (P/NP-Eq.)
• BooMS reimplemented in EBat as the original wouldn’t work

​

​

16

​

​

Reusing BooM’s SAT Encoding

17

​

​

EBatP (Picker)

18

All Mappings

(Mismatches and matches)

​

Miter

(SAT instance)

​

​

EBatP (Picker)

19

All Mappings

(Mismatches and matches)

​

UnSAT(match)

SAT (mismatch)

Next map

​

​

EBatP (Picker)

20

All Mappings

(Mismatches and matches)

​

UnSAT(match)

SAT (mismatch)

New generalization

(P/NP-Equivalence)

New mismatch blocking

(P-Equivalence)

Next map

Performance breakthrough for P-Equivalence!

​

​

EBatP (Picker)

21

All Mappings

(Mismatches and matches)

​

UnSAT(match)

SAT (mismatch)

Strengthening(Core)

Block Match

Report

Next map

Performance breakthrough

for P/NP-Equivalence!

​

​

EBatP (Picker)

22

All Mappings

(Mismatches and matches)

​

No more mappings!

​

​

EBatC in High-Level

23

EBatP

BooMS

​

​

EBatC vs EBatP

24

8/12/2025

​

​

Generalization in Boolean Matching

25

8/12/2025

[Fried, Nadel, Sebastiani, Shalmon, SAT’24]

​

​

Generalization under NP-Equivalence

26

8/12/2025

1

0

​

​

Generalization under NP-Equivalence

27

8/12/2025

Generalization

1

0

​

​

Generalization under P-Equivalence

28

8/12/2025

​

​

Experimental Results

• In total, we tested 388 benchmarks originating from:
• ITC’99 (used in BooM paper)
• ICCAD’23 Contest
• EPFL + ISCAS’85
• We split multi-output circuits into single-output instances
• We evaluated:
• Solved instances (Timeout of 60s)
• PAR-2 score (Run-time if solved; 2*Timeout if not solved)

​

• We use IntelSAT for all SAT queries and CaDiCaL for UnSAT core extraction

​

​

​

​

​

​

29

​

​

Results

30

New

New

​

​

Results

31

​

​

Results

32

​

​

Conclusion & Future Work

• We presented EBat, an open-source tool for All Boolean Matching:
• New high-level algorithms and critical subroutines
• Solves 3-4x more benchmarks than the baseline

​

Future work:

• Handle multiple outputs and sequential circuits
• Implement circuit preprocessing techniques

​

​

33

​

​

Thank you for listening

​

Questions?

​

​

Results

​

​

​

​

​

35

​

​

EBatC in High Level

36

Mismatch Bucket

​

Miter

Generalization

Block Mis

EBatP

BoomS High-Level Flow

​

​

How BooMS works:

37

Mismatches Bucket

​

Miter

​

​

How BooMS works:

38

Mismatches Bucket

​

Miter

Next mismatch

​

​

How BooMS works:

39

Mismatches Bucket

​

Miter

Generalization

Next mismatch

​

​

How BooMS works:

40

Mismatches Bucket

​

Miter

Generalization

Block Mismatches

Next mismatch

​

​

How BooMS works:

41

Mismatches Bucket

​

Miter

No more mismatches!

​

​

How BooMS works:

42

Mismatches Bucket

​

Miter

Next ; Report

Block Match

All Matches!

​

​