  Boolean Skolem function synthesis concerns synthesizing outputs as Boolean
functions of inputs such that a relational specification between inputs and
outputs is satisfied. This problem, also known as Boolean functional synthesis,
has several applications, including design of safe controllers for autonomous
systems, certified QBF solving, cryptanalysis etc. Recently, complexity
theoretic hardness results have been shown for the problem, although several
algorithms proposed in the literature are known to work well in practice. This
dichotomy between theoretical hardness and practical efficacy has motivated the
research into normal forms or representations of input specifications that
permit efficient synthesis, thus explaining perhaps the efficacy of these
algorithms.
  In this paper we go one step beyond this and ask if there exists a normal
form representation that can in fact precisely characterize "efficient"
synthesis. We present a normal form called SAUNF that precisely characterizes
tractable synthesis in the following sense: a specification is polynomial time
synthesizable iff it can be compiled to SAUNF in polynomial time. Additionally,
a specification admits a polynomial-sized functional solution iff there exists
a semantically equivalent polynomial-sized SAUNF representation. SAUNF is
exponentially more succinct than well-established normal forms like BDDs and
DNNFs, used in the context of AI problems, and strictly subsumes other more
recently proposed forms like SynNNF. It enjoys compositional properties that
are similar to those of DNNF. Thus, SAUNF provides the right trade-off in
knowledge representation for Boolean functional synthesis.
