提出可满足性理论中函数合成的新方法，解决复杂度问题并给出高效求解形式。
Presburger Functional Synthesis: Complexity and Tractable Normal Forms
- 针对Presburger算术提出函数合成算法，证明其时间复杂度为EXPTIME
- 发现一类特殊规范形式PSyNF，使合成可在多项式时间内完成
- 该方法适合形式化验证与自动程序生成场景，尤其适用于数学约束系统
给定输入与输出之间的关系逻辑公式，函数合成的目标是自动生成一个满足该关系的函数。本文首次系统研究了在Presburger算术理论下的函数合成问题（称为PFnS）。我们证明PFnS可在EXPTIME内求解，并给出了匹配的指数下界，这与布尔函数合成仅知条件性指数下界不同。进一步发现，当仅有一个输入和一个输出变量时，PFnS的复杂度等价于一般布尔函数合成。随后，我们定义了一种特殊规范形式PSyNF，保证了PFnS在多项式时间与多项式大小内可解。论文还证明了PSyNF的可判定性与转换机制，并说明任何能保证多项式可解的其他形式均可在多项式时间内转化为PSyNF。最后，我们提出一种更易检验但指数更不紧凑的语法规范形式。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。