Abstract
Given a Boolean relational specification \varphi(X, Y) with inputs X and outputs Y, the functional synthesis problem asks us to express Y as functions F(X) such that \varphi(X, F(X)) holds whenever \exists Y \varphi(X, Y) holds. While this problem is intractable in general, it is known that if the specification is represented in special circuit forms, the problem admits efficient solutions. In this talk, we ask if the converse is also true, i.e. whenever a class of specifications admits efficient synthesis, does the class have specific representational properties? We answer this question positively by showing a class C* of Boolean circuits with the following properties: (a) Every relational specification can be compiled to C* (b) Every specification in C* admits polynomial-time synthesis (c) For every class C of circuit-based specifications, C admits polynomial-time synthesis iff there exists a polynomial-time compilation of C to C*. Similarly, C admits polynomial-sized solutions iff for every specification in C, there is a polynomial-sized equivalent specification in C*. This provides a characterization of when Boolean functional synthesis is efficiently solvable. We study properties of the class C* and outline a simple algorithm to compile a CNF formula to a circuit in C*.