• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Engineering an Efficient Boolean Functional Synthesis Engine.
Priyanka Golia, Friedrich Slivovsky, Subhajit Roy and Kuldeep S. Meel.
In Proceedings of IEEE/ACM International Conference on Computer-Aided Design (ICCAD), November 2021.
Best Paper Award Nomination
Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state of-the-art approach combines machine learning and automated reasoning to synthesise Boolean functions efficiently. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We integrate these improvements into the state-of-the-art frame- work, called Manthan. The resulting framework, Manthan2, shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan - an increment of 153 instances over the state of-the-art. To put this into perspective, Manthan improved on the prior state of the art by only 76 instances.
@inproceedings{GSRM21,
title={Engineering an Efficient Boolean Functional Synthesis Engine},
author={Golia, Priyanka and Slivovsky, Friedrich and Roy, Subhajit and Meel, Kuldeep S.},
booktitle=ICCAD,
year={2021},
month=nov,
bib2html_dl_pdf={../Papers/iccad21.pdf},
bib2html_rescat={Synthesis},
note={Best Paper Award Nomination},
bib2html_pubtype={Refereed Conference,Award Winner},
abstract={Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state of-the-art approach combines machine learning and automated reasoning to synthesise Boolean functions efficiently. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates.
We integrate these improvements into the state-of-the-art frame- work, called Manthan. The resulting framework, Manthan2, shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan - an increment of 153 instances over the state of-the-art. To put this into perspective, Manthan improved on the prior state of the art by only 76 instances.},
area={ar},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51