Engineering an Efficient Boolean Functional Synthesis Engine

TL;DR

This paper introduces four algorithmic improvements to a data-driven Boolean functional synthesis framework, significantly enhancing its scalability and efficiency, enabling it to solve more complex benchmarks than previous methods.

Contribution

The paper presents Manthan2, an improved synthesis framework with four key algorithmic enhancements that outperform the previous state-of-the-art in Boolean functional synthesis.

Findings

Manthan2 solves 509 out of 609 benchmarks, surpassing Manthan's 356.

Four algorithmic improvements lead to doubled problem-solving capacity.

Significant runtime performance improvements over previous methods.

Abstract

Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reasoning to efficiently synthesise Boolean functions. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We implement these improvements in the state-of-the-art framework, called Manthan. The proposed framework is called Manthan2. Manthan2 shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan--- an increment of 153 instances over the state-of-the-art. To put this into perspective, Manthan improved on the prior state-of-the-art by only 76 instances.