BooM: A decision procedure for boolean matching with abstraction and dynamic learning

Boolean matching determines whether two given (in)completely-specified Boolean functions can be identical or complementary to each other under permutation and/or negation of their input variables. Due to its broad applications in logic synthesis and verification, it attracted much attention. Most prior efforts however were incomplete and/or restricted to certain special matching conditions. In contrast, this paper focuses on the computation kernel of Boolean matching and proposes a complete generic framework. Through conflict-driven learning and abstraction, the capacity of Boolean matching scales up due to the effective pruning of infeasible matching solutions. Experiments show encouraging results in resolving hard instances that are otherwise unsolvable.