Presburger Functional Synthesis: Complexity and Normal Forms
COM3 Level 2
MR25, COM3 02-70
Abstract:
Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this talk, we look at this problem for the theory of Presburger Arithmetic. We show that Presburger Functional Synthesis (PFnS) can be solved in EXPTIME and provide a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Further, we show that PFnS for one input and one output variable is as hard as BFnS in general. We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS. We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF. This is joint work with S. Akshay, Georg Zetsche and A.R. Balasubramanian, and appeared in KR 2025.
Bio:
Supratik Chakraborty is Bajaj Group Chair Professor of Computer Science and Engineering at IIT Bombay. His research interests lie at the intersection of theoretical and applied computer science, with a focus on scalable and practical formal methods. He has worked in the past on constrained sampling and counting, automated synthesis, formal verification, automata theory and logic. He is a Fellow of Indian National Academy of Engineering, a Distinguished Member of ACM, and a Distinguished Alumnus of IIT Kharagpur.