Pushing The Envelope for Boolean Functional Synthesis

Boolean functional synthesis using AIGs and CEGAR has been recently proposed as a promising alternative to synthesis based on BDDs or on DPLL+CDCL style clausal reasoning. In this paper, we delve deeper into the AIG+CEGAR approach and propose techniques that significantly improve the performance of Boolean functional synthesis, sometimes by orders of magnitude vis-a-vis state-of-the-art tools. This is achieved by a combination of algorithmic modifications resulting from an improved theoretical analysis of the AIG+CEGAR approach. Our approach also harnesses the power of recently proposed efficient almost-uniform samplers to improve the performance of synthesis. Empirical evaluation on a suite of benchmarks shows that our approach outperforms existing state-of-the-art Boolean functional synthesis tools on most of these benchmarks.