Boolean Functional Synthesis: A View from Theory and Practice

It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing it requires us to take a functional view, i. e. , to have functions that produce outputs from inputs. Can we automatically synthesize such functions from a given relational specification? In this tutorial, we focus on this question in the Boolean setting: given a relation between Boolean inputs and outputs as the specification, the Boolean functional synthesis problem asks to synthesize each output as a function of the inputs such that the specification is met. We start by showing the centrality of this problem via multiple examples and applications in a variety of domains ranging from program synthesis to planning. We then look at theoretical hardness results and survey some of the algorithmic techniques that have been developed in recent years to tackle this problem, remarking on their surprising practical performance. This leads us to examine the structure of specification in more depth and doing so we develop a theory of knowledge representations and new algorithmic directions. We end with several open questions and avenues for future work.

Authors

• S. Akshay Indian Institute of Technology Bombay, Mumbai, India

Keywords

No keywords are indexed for this paper.