Abstract

Suppose we want to design a system with inputs X and outputs Y, such that the relation between X and Y is specified as a Boolean formula \varphi(X, Y).  The problem of synthesizing Y as a function of X, say F(X),  s.t. that \varphi(X, F(X)) holds for all X is the classical synthesis problem.  We augment this problem definition to include cases where the specification is  ”unrealizable” in the classical sense, i.e. there exist some values of X for which no value of Y satisfies the spec.  Specificially, we ask if we can synthesize Y as a function F(X) such that \varphi(X, F(X)) holds for all values of X for which \exists Y \varphi(X, Y) holds.  It turns out thatthere are many interesting applications where this notion of synthesis is useful.  We present an overview of two different approaches that have been recently proposed to solve the above problem—one based on an iterative repair algorithm, and the other based on knowlege compilation. We present results obtained from each of these approaches and outline some future directions of research.