• 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 Thu Sep 10, 2026 16:32:38