Improving the creation of AIGs from reactive synthesis

In the SYNTCOMP competition, correct hardware independent logic networks in the form of AIGs need to be created from logic descriptions. Knor, a participating program that creates such solutions, converts during a final stage its BDD to AIG which can be optimized. In this paper multiple AIG minimization techniques are explored and benchmarked. A generally applicable AIG minimization strategy is found with the benchmarks, and the possibility of merging this with the initial creation of the AIG is discussed.