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 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.
Synthesis of Boolean Networks from Biological Dynamical Constraints using Answer-Set Programming
LRI, CNRS, U. Paris-Sud U. Paris-Saclay（巴黎-萨克雷大学南巴黎校区法国国家科学研究中心计算机研究所）；LaBRI, CNRS, U. Bordeaux Bordeaux INP（波尔多大学波尔多国立理工学院法国国家科学研究中心计算机与自动化研究所）；Institut Curie, INSERM U. PSL, Mines ParisTech（巴黎文理研究大学法国国家健康与医学研究院巴黎高等矿业学院居里研究所）
Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis
St. Petersburg State University（圣彼得堡国立大学）；Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences（俄罗斯科学院圣彼得堡斯捷克洛夫数学研究所）；ITMO University（圣彼得堡国立信息技术机械与光学大学）；Neapolis University Pafos（帕福斯尼阿波利斯大学）；JetBrains Research（JetBrains研究院）
Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
D-CHAB, ETH Zurich, Zurich, Switzerland.；D-INFK, ETH Zurich, Zurich, Switzerland.；ETH AI Center, Zurich, Switzerland.；University of Pennsylvania, PA, USA.；Independent Researcher.
