Presburger Functional Synthesis: Complexity and Tractable Normal Forms

• URL: http://arxiv.org/abs/2508.07207v1
• Date: Sun, 10 Aug 2025 07:00:34 GMT
• Title: Presburger Functional Synthesis: Complexity and Tractable Normal Forms
• Authors: S. Akshay, A. R. Balasubramanian, Supratik Chakraborty, Georg Zetzsche,
• Abstract summary: We show that Presburger Functional Synthesis (PFnS) can be solved in EXPTIME and provide a matching exponential lower bound.<n>We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS.<n>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.
• Score: 0.4499833362998487
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• FUTON: Fourier Tensor Network for Implicit Neural Representations [56.48739018255443]
  Implicit neural representations (INRs) have emerged as powerful tools for encoding signals, yet dominant-based designs often suffer from slow convergence, overfitting to noise, and poor extrapolation.<n>We introduce FUTON, which models signals as generalized Fourier series whose coefficients are parameterized by a low-rank tensor decomposition.
  arXiv  Detail & Related papers  (2026-02-13T19:31:44Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Explicit Solution Equation for Every Combinatorial Problem via Tensor Networks: MeLoCoToN [55.2480439325792]
  We show that every computation problem has an exact explicit equation that returns its solution.<n>We present a method to obtain an equation that solves exactly any problem, both inversion, constraint satisfaction and optimization.
  arXiv  Detail & Related papers  (2025-02-09T18:16:53Z)
• Compilation and Fast Model Counting beyond CNF [31.620928650659586]
  This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF.<n>The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings.<n>We give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.
  arXiv  Detail & Related papers  (2025-02-01T14:00:04Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Evolutionary Construction of Perfectly Balanced Boolean Functions [7.673465837624365]
  We investigate the use of Genetic Programming (GP) and Genetic Algorithms (GA) to construct Boolean functions that satisfy a property, perfect balancedness, along with a good nonlinearity profile. Surprisingly, the results show that GA with the weightwise balanced representation outperforms GP with the classical truth table phenotype in finding highly nonlinear WPB functions.
  arXiv  Detail & Related papers  (2022-02-16T18:03:04Z)
• Interactive Proofs for Synthesizing Quantum States and Unitaries [0.15229257192293197]
  We study the complexity of inherently quantum operations such as constructing quantum states or performing unitary transformations. We define models of interactive proofs for quantum states and unitaries. We obtain analogous results in the setting with multiple entangled provers as well.
  arXiv  Detail & Related papers  (2021-08-16T15:59:33Z)
• A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis [2.093287944284448]
  We present a form of representation called SAUNF that characterizes a normal synthesis in a tractable way. It is exponentially more succinct than well-established normal forms like BDDs and DNNFs, used in the context of AI problems, and strictly subsumes other more recently proposed forms like SynNNF.
  arXiv  Detail & Related papers  (2021-04-29T04:16:41Z)
• Finite-Function-Encoding Quantum States [52.77024349608834]
  We introduce finite-function-encoding (FFE) states which encode arbitrary $d$-valued logic functions. We investigate some of their structural properties.
  arXiv  Detail & Related papers  (2020-12-01T13:53:23Z)
• On Function Approximation in Reinforcement Learning: Optimism in the Face of Large State Spaces [208.67848059021915]
  We study the exploration-exploitation tradeoff at the core of reinforcement learning. In particular, we prove that the complexity of the function class $mathcalF$ characterizes the complexity of the function. Our regret bounds are independent of the number of episodes.
  arXiv  Detail & Related papers  (2020-11-09T18:32:22Z)
• A tetrachotomy of ontology-mediated queries with a covering axiom [1.749935196721634]
  Our concern is the problem of efficiently determining the data complexity of answering queries mediated by description and their optimal rewritings to standard database queries. We focus on Boolean conjunctive-mediated queries called disjunctive sirups (or d-sirups) Some d-sirups only have exponential-size resolution features, some only double-exponential-size positive existential existential-rewritings and single-exprecursive datalog rewritings.
  arXiv  Detail & Related papers  (2020-06-07T14:47:07Z)
• On estimating the entropy of shallow circuit outputs [49.1574468325115]
  Estimating the entropy of probability distributions and quantum states is a fundamental task in information processing. We show that entropy estimation for distributions or states produced by either log-depth circuits or constant-depth circuits with gates of bounded fan-in and unbounded fan-out is at least as hard as the Learning with Errors problem.
  arXiv  Detail & Related papers  (2020-02-27T15:32:08Z)
• Learning Likelihoods with Conditional Normalizing Flows [54.60456010771409]
  Conditional normalizing flows (CNFs) are efficient in sampling and inference. We present a study of CNFs where the base density to output space mapping is conditioned on an input x, to model conditional densities p(y|x)
  arXiv  Detail & Related papers  (2019-11-29T19:17:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.