Blazing Fast Skolem 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. With B∃SS, we intend to 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.
What's hard about Boolean Functional Synthesis?
S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, Shetal Shah.
30th International Conference on Computer Aided Verification (CAV 2018)
Pushing The Envelope for Boolean Function Synthesis
S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, Shetal Shah.
CSE IITB Technical Report (TR-CSE-2017-87)
B∃SS can be downloaded from https://github.com/Sumith1896/bfss
A project led by Supratik Chakraborty, B∃SS is developed with ♥ at IIT Bombay.
(from left to right) Shubham, Akshay, Supratik, Shetal and Sumith
Picture credits: Blaise Genest