Alladi Ramakrishnan Hall

Knowledge Compilation for Boolean Functional Synthesis

Supratik Chakraborty

Indian Institute of Technology, Mumbai

Given a Boolean specification F(X, Y), where X is a vector of Boolean *outputs* and Y is a vector of Boolean *inputs*, the Boolean Functional Synthesis problem asks for a function vector G(Y), of the same dimension as X, such that \forall Y ( \exists X F(X, Y) \leftrightarrow F(G(Y), Y) ). This problem has several applications, e.g. in certified QBF SAT, in reactive synthesis, disjunctive decomposition of relations etc. In this talk, we will discuss some hardness results pertaining to how large G(Y) can be. We also show that if F(X, Y) is represented in a certain normal form, then synthesis can be accomplished in poly-time (and hence in poly-size). We show exponential gaps between this representation form and some other related representation forms studied in the knowledge compilation literature (like BDDs and dDNNF). We also show that every specification that admits a small vector G(Y) as solution necessarily admits a refinement that is small in the proposed representation form.