@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
  },
}