# Presburger Functional Synthesis: Complexity and Tractable Normal Forms

arXiv: https://arxiv.org/abs/2508.07207 · HTML: https://mlsanity.com/paper/2508.07207/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 40 references that are in the map.
- First posted on arXiv 10 Aug 2025.

## Builds on (most cited first, 8 of 8)

- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [Knowledge Compilation for Boolean Functional Synthesis](https://mlsanity.com/paper/1908.06275/) (2019)
- [Skolem Functions for Factored Formulas](https://mlsanity.com/paper/1508.05497/) (2015)
- [Functional Synthesis via Input-Output Separation](https://mlsanity.com/paper/1808.08190/) (2018)
- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy](https://mlsanity.com/paper/1401.5266/) (2014)
- [A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis](https://mlsanity.com/paper/2104.14098/) (2021)
- [An efficient quantifier elimination procedure for Presburger arithmetic](https://mlsanity.com/paper/2405.01183/) (2024)

## Abstract (arXiv)

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.