# Engineering an Efficient Boolean Functional Synthesis Engine

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 52 references that are in the map.
- First posted on arXiv 12 Aug 2021.

## Builds on (most cited first, 7 of 7)

- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [What's hard about Boolean Functional Synthesis](https://mlsanity.com/paper/1804.05507/) (2018)
- [Knowledge Compilation for Boolean Functional Synthesis](https://mlsanity.com/paper/1908.06275/) (2019)
- [Skolem Functions for Factored Formulas](https://mlsanity.com/paper/1508.05497/) (2015)
- [Towards Parallel Boolean Functional Synthesis](https://mlsanity.com/paper/1703.01440/) (2017)
- [Understanding and Extending Incremental Determinization for 2QBF](https://mlsanity.com/paper/1905.13411/) (2019)

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

- [Lightweight Online Learning for Sets of Related Problems in Automated Reasoning](https://mlsanity.com/paper/2305.11087/) (2023)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)
- [Presburger Functional Synthesis: Complexity and Tractable Normal Forms](https://mlsanity.com/paper/2508.07207/) (2025)

## Abstract (arXiv)

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.