Towards Parallel Boolean Functional Synthesis

TL;DR

This paper introduces the first parallel method for Boolean functional synthesis, leveraging compositional and CEGAR-style reasoning, significantly improving performance on benchmark problems.

Contribution

It presents a novel parallel approach to Boolean functional synthesis, combining compositional and CEGAR techniques, outperforming existing tools.

Findings

Outperforms existing tools on benchmark problems

Uses compositional and CEGAR-style reasoning effectively

Demonstrates scalability and efficiency improvements

Abstract

Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.