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

AIGs found successful use in diverse EDA applications. A well-tuned combination of AIGs and boolean satisfiability made an impact on formal verification, including both model checking