• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Manthan: A Data-Driven Approach for Boolean Function Synthesis.
Priyanka Golia, Subhajit Roy and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2020.
Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development, a large number of problems remain beyond the reach of the current state of the art techniques.Motivated by the progress in machine learning, we propose Manthan, a novel data-driven approach to Boolean functional synthesis. Manthan views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. Furthermore, Manthan solves 60 benchmarks that none of the current state of the art techniques could solve. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.
@inproceedings{GRM20a,
title={Manthan: A Data-Driven Approach for Boolean Function Synthesis},
author={Golia, Priyanka and Roy, Subhajit and Meel, Kuldeep S.},
bib2html_pubtype={Refereed Conference},
booktitle=CAV,
month=jul,
bib2html_dl_pdf={../Papers/cav20-grm.pdf},
year={2020},
bib2html_rescat={Synthesis},
abstract={Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development,
a large number of problems remain beyond the reach of the current state of the art techniques.
Motivated by the progress in machine learning, we propose Manthan, a novel data-driven approach to Boolean functional
synthesis. Manthan views functional synthesis as a classification problem, relying on advances in constrained sampling
for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification.
On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the
current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art
technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art.
Furthermore, Manthan solves 60 benchmarks that none of the current state of the art techniques could solve. The significant
performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51