And-inverter graph

For example, ΣoΠs are circuits with at most two levels while BDDs are canonical, that is, they require that input variables be evaluated in the same order on all paths.

Several important techniques were discovered early at IBM, such as combining and reusing multi-input logic expressions and subexpressions, now known as structural hashing.

[citation needed] Another important development was the recent emergence of much more efficient boolean satisfiability (SAT) solvers.

When coupled with AIGs as the circuit representation, they lead to remarkable speedups in solving a wide variety of boolean problems.

[6] There is a growing understanding that logic and physical synthesis problems can be solved using simulation and boolean satisfiability to compute functional properties (such as symmetries)[7] and node flexibilities (such as don't-care terms, resubstitutions, and SPFDs).

[11] Ongoing research includes implementing a modern logic synthesis system completely based on AIGs.