Boolean Functional Synthesis: Hardness and Practical Algorithms |
|
---|---|
![]() Prof. Supratik Chakraborty, CSE, IIT Bombay
Short Bio: Date: May 27, 2020; Thursday |
Abstract:
Given a Boolean relation between inputs and outputs, Boolean Functional Synthesis seeks to represent the outputs as deterministic functions of the inputs. This problem, also known as Skolem function synthesis, has a wide range of applications, and is one of the key components of reactive controller synthesis techniques. An efficient solution to this problem can be shown to yield an efficient algorithm for prime factorization, thereby cracking RSA. In this talk, we will first present (conditional) lower bounds on the hardness of the problem, thereby showing that it is unlikely that there are time or space efficient algorithms for Boolean Functional Synthesis. We will then present work done in our group on developing algorithms that are practically efficient on a large class of benchmarks. This includes expansion-based algorithms and knowledge-compilation based algorithms. We will also discuss some intuition on why these algorithms work well in practice. Finally, we will discuss experimental results that illustrate the practical effectiveness of the algorithms and conclude by identifying key challenges in the road ahead.
|