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.

研究 Boolean functional synthesis 问题中 CNF 转化为 SynNNF 的算法，并证明 SynNNF 具有多项式时间综合的优势。