Presburger Functional Synthesis: Complexity and Tractable Normal Forms

TL;DR

This paper investigates the complexity of Presburger functional synthesis, establishing its EXPTIME solvability, identifying a normal form for efficient synthesis, and comparing it to Boolean synthesis in terms of difficulty and normal forms.

Contribution

The paper introduces Presburger Functional Synthesis, proves its EXPTIME complexity, and identifies a normal form (PSyNF) that enables polynomial-time solutions, advancing understanding of synthesis in Presburger arithmetic.

Findings

PFnS can be solved in EXPTIME with a matching lower bound.

PSyNF guarantees polynomial-time and polynomial-size synthesis.

PFnS for one input/output variable is as hard as Boolean synthesis.

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 paper, we launch an investigation of this problem for the theory of Presburger Arithmetic, that we call Presburger Functional Synthesis (PFnS). We show that 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. Finally, we identify a syntactic normal form that is easier to check but is exponentially less succinct than PSyNF.