Presburger Functional Synthesis: Complexity and Normal Forms

May 22 10:30 ₂₀₂₆

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 will discuss this problem for the theory of Presburger Arithmetic. We will show that Presburger Functional Synthesis (PFnS) can be solved in EXPTIME, and discusss 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 will discuss why PFnS for one input and one output variable is already as hard as BFnS in general. Finally, we will identify a special normal form, called PSyNF, for the specification formula that guarantees polynomial-time and polynomial-size solvability of PFnS. We will discuss interesting properties of PSyNF, including how to check and compile to this form, and conditions under which any form that guarantees polynomial-time solvability of PFnS can be compiled in polynomial-time to PSyNF.

This is joint work with S. Akshay, Georg Zetsche and A.R. Balasubramanian, and appeared in KR 2025.