# Knowledge Compilation for Boolean Functional Synthesis

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Aug 2019.

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

- [Tractable Boolean and Arithmetic Circuits](https://mlsanity.com/paper/2202.02942/) (2022)
- [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)
- [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 formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever exists X F(X,Y) holds. In this paper, we investigate the relation between the representation of the specification F(X,Y) and the complexity of synthesis. We introduce a new normal form for Boolean formulas, called SynNNF, that guarantees polynomial-time synthesis and also polynomial-time existential quantification for some order of quantification of variables. We show that several normal forms studied in the knowledge compilation literature are subsumed by SynNNF, although SynNNFcan be super-polynomially more succinct than them. Motivated by these results, we propose an algorithm to convert a specification in CNF to SynNNF, with the intent of solving the Boolean functional synthesis problem. Experiments with a prototype implementation show that this approach solves several benchmarks beyond the reach of state-of-the-art tools.