Boolean Functional Synthesis using Gated Continuous Logic Networks

Abstract

Boolean Functional Synthesis (BFS) is a well-known challenging problem in the domain of automated program synthesis from logical specifications. This problem aims to synthesize a Boolean function that is correct-by-construction with respect to the declared specification; this specification symbolically relates the inputs and outputs of the function to be synthesized. Since Boolean functions are the basic building blocks of modern digital systems, BFS has applications in a wide range of areas, including QBF-SAT solving, circuit repair and debugging. This has motivated the community to develop practically efficient algorithms for synthesizing compact Boolean functions, which is a non-trivial endeavor. However, to the best of our knowledge, current techniques are unable to specify a bound on the Boolean function size during synthesis. Specifying a bound on the size of the formula offers flexibility in synthesizing minimal-sized Boolean functions.

Learning Boolean functions from logical specifications using neural networks is a difficult problem as it requires the network to represent Boolean functions. Boolean functions are discrete functions and consequently, non-differentiable. Thus, learning a Boolean function directly using traditional neural networks is not possible. Recently Ryan et al proposed the Gated Continuous Logic Network (GCLN) model that builds on Fuzzy Logic to represent Boolean and linear integer operator, in the context of learning invariants for programs. In this work, we investigate the use of the GCLN model to synthesize solutions to the BFS problem. Our model lets us bound the number of clauses used in the synthesized Boolean function.

We implement this approach in our tool BNSynth (for Bounded Neural Synthesis) which also uses sampling and counter-example-guided techniques to synthesize Boolean functions. We validate our hypothesis that this system can learn smaller functions as compared to a state-of-the-art tool over custom benchmarks and LUT-based benchmarks from the ISCAS85 benchmark suite. We observe a 15.8X average improvement in formula size by the number of clauses for these benchmarks. This empirically shows that our system can synthesize smaller Boolean functions compared to the state-of-the-art.