Characterizing Boolean Functional Synthesis via Knowledge Representation

Boolean functional synthesis concerns synthesizing out1 puts as Boolean functions of inputs such that a rela2 tional specification between inputs and outputs is sat3 isfied. This has several applications, including design 4 of safe controllers for autonomous systems, certified 5 QBF solving, cryptanalysis etc. Despite complexity6 theoretic hardness results, several algorithms proposed 7 in the literature are known to work well in practice. 8 This motivates the investigation of whether there exist 9 representations of input specifications that permit and 10 also characterize efficient synthesis. 11 In this paper, we present a normal form called SAUNF 12 that precisely characterizes tractable synthesis in the 13 following sense: a specification is polynomial time syn14 thesizable iff it can be compiled to SAUNF in poly15 nomial time. Additionally, a specification admits a 16 polynomial-sized functional solution iff there exists a 17 semantically equivalent polynomial-sized SAUNF rep18 resentation. SAUNF is exponentially more succinct 19 than well-established normal forms like BDDs and 20 DNNFs, used in the context of AI problems, and 21 strictly subsumes other more recently proposed forms. 22 It enjoys compositional properties that are similar to 23 those of DNNF. Thus, SAUNF provides the right trade24 off in knowledge representation for Boolean functional 25 synthesis. 26