# What's hard about Boolean Functional Synthesis

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Apr 2018.

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

- [Humans in 4D: Reconstructing and Tracking Humans with Transformers](https://mlsanity.com/paper/2305.20091/) (2023)
- [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)
- [Program Synthesis as Dependency Quantified Formula Modulo Theory](https://mlsanity.com/paper/2105.09221/) (2021)
- [BNSynth: Bounded Boolean Functional Synthesis](https://mlsanity.com/paper/2212.08170/) (2022)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)

## Abstract (arXiv)

Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is met. In this paper, we first show that unless some hard conjectures in complexity theory are falsified, Boolean functional synthesis must necessarily generate exponential-sized Skolem functions, thereby requiring exponential time, in the worst-case. Given this inherent hardness, what does one do to solve the problem? We present a two-phase algorithm for Boolean functional synthesis, where the first phase is efficient both in terms of time and sizes of synthesized functions, and solves an overwhelming majority of benchmarks. To explain this surprisingly good performance, we provide a sufficient condition under which the first phase must produce exact correct answers. When this condition fails, the second phase builds upon the result of the first phase, possibly requiring exponential time and generating exponential-sized functions in the worst-case. Detailed experimental evaluation shows our algorithm to perform better than state-of-the-art techniques for a majority of benchmarks.