# Towards Parallel Boolean Functional Synthesis

arXiv: https://arxiv.org/abs/1703.01440 · HTML: https://mlsanity.com/paper/1703.01440/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Mar 2017.

## Built on by (most cited first, 4 of 4)

- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis](https://mlsanity.com/paper/2104.14098/) (2021)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)

## Abstract (arXiv)

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.