The "FRAIG" algorithm is pretty cool. To find equivalent nodes in an And/Inverter graph (e.g., a hardware circuit), it operates by... (1) simulating the graph

The "FRAIG" algorithm is pretty cool. To find equivalent nodes in an And/Inverter graph (e.g., a hardware circuit), it operates by... (1) simulating the graph on random numbers to identify nodes that might be equivalent (this can be done with huge parallelism by using wide, bitwise and/not operations) (2) using SAT to determine if these candidates really are equivalent (3) building a new network that canonicalizes all of the nodes you've found to be equivalent. It can be a really effective pre-processing step for many kinds of circuit analysis. https://people.eecs.berkeley.edu/~alanmi/courses/2005_290A/papers/fraigs03.pdf https://people.eecs.berkeley.edu/~alanmi/courses/2005_290A/p...