# Knowledge Compilation for Boolean Functional Synthesis

## TL;DR

This paper introduces SynNNF, a new normal form for Boolean formulas that enables polynomial-time synthesis and quantification, improving the efficiency of Boolean functional synthesis and solving benchmarks beyond current tools.

## Contribution

The paper presents SynNNF, a novel normal form that guarantees efficient synthesis and quantification, and proposes an algorithm to convert CNF formulas into SynNNF for practical synthesis.

## Key findings

- SynNNF can be more succinct than existing normal forms.
- The conversion algorithm enables solving complex benchmarks.
- Prototype implementation outperforms state-of-the-art tools.

## Abstract

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.