{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:59:47Z","timestamp":1762325987412,"version":"build-2065373602"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:p>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\n\nlaunch 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\n\nand 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\n\nguarantees 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\n\nother 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.<\/jats:p>","DOI":"10.24963\/kr.2025\/2","type":"proceedings-article","created":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:10:44Z","timestamp":1762323044000},"page":"12-23","source":"Crossref","is-referenced-by-count":0,"title":["Presburger Functional Synthesis: Complexity and Tractable Normal Forms"],"prefix":"10.24963","author":[{"given":"S.","family":"Akshay","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Bombay"}]},{"given":"A. R.","family":"Balasubramanian","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems Kaiserslautern"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bombay"}]},{"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems Kaiserslautern"}]}],"member":"10584","event":{"name":"22nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2025}","theme":"Artificial Intelligence","location":"Melbourne, Australia","acronym":"KR-2025","number":"22","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"start":{"date-parts":[[2025,11,11]]},"end":{"date-parts":[[2025,11,17]]}},"container-title":["Proceedings of the TwentySecond International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:10:46Z","timestamp":1762323046000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2025\/2"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2025,11]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2025\/2","relation":{},"subject":[],"published":{"date-parts":[[2025,11]]}}}