BNSynth: Bounded Boolean Functional Synthesis
Ravi Raja (1), Stanly Samuel (1), Chiranjib Bhattacharyya (1), Deepak, D'Souza (1), Aditya Kanade (2) ((1) Indian Institute of Science, Bangalore,, (2) Microsoft Research, Bangalore)

TL;DR
BNSynth introduces a neural-guided, bounded approach to Boolean functional synthesis, producing smaller solutions with significant size reductions, applicable in resource-constrained design scenarios.
Contribution
First tool to solve Boolean Functional Synthesis with a solution space bound, enabling smaller, resource-efficient Boolean functions.
Findings
Achieves 3.2X to 24X reduction in solution size compared to existing tools.
Uses counter-example guided neural approach for bounded BFS.
Demonstrates promising results on benchmark problems.
Abstract
The automated synthesis of correct-by-construction Boolean functions from logical specifications is known as the Boolean Functional Synthesis (BFS) problem. BFS has many application areas that range from software engineering to circuit design. In this paper, we introduce a tool BNSynth, that is the first to solve the BFS problem under a given bound on the solution space. Bounding the solution space induces the synthesis of smaller functions that benefit resource constrained areas such as circuit design. BNSynth uses a counter-example guided, neural approach to solve the bounded BFS problem. Initial results show promise in synthesizing smaller solutions; we observe at least \textbf{3.2X} (and up to \textbf{24X}) improvement in the reduction of solution size on average, as compared to state of the art tools on our benchmarks. BNSynth is available on GitHub under an open source license.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Engineering Research · Software Testing and Debugging Techniques
