Regular integer linear-exponential programming (RegILEP) asks whether a system of inequalities of the form $\sum\nolimits_{i = 1..n} {\left({{a_i}\cdot{x_i} + {b_i}\cdot{2^{{x_i}}}}\right)} \leq c$, where all coefficients are integers, has a solution in the integers whose binary representations belong to some regular set over the alphabet {0,1}. RegILEP has recently been proved decidable in ExpSpace using purely automata-theoretic techniques. The first contribution of the paper is a novel decision procedure for RegILEP, which works in a quantifier elimination fashion: after specifying a total order on the variables, the procedure gradually excludes the exponential occurrences of the leading variable and then eliminates the linear ones. This decision procedure meets the existing ExpSpace upper bound for the problem. As a complementary result, we show that regular integer linear programming for the domain defined by the regular expression (00∪01)*is PSPACE-complete.

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function x ↦ t ⋅ x, where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions x ↦ ⌊x/(f(t))⌋, one for each integer polynomial f. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring ℤ[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.

This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms $2^x$ and remainder terms ${(x \bmod 2^y)}$. Our result implies that the existential theory of the structure $(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$ has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function $x \mapsto 2^x$ and the binary predicate $V_2(x,y)$ that is true whenever $y \geq 1$ is the largest power of $2$ dividing $x$. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).

Abstract This paper presents a similar approach for existential first-order characterizations of the languages recognizable by finite automata, by Parikh automata, and by multi-counter machines over the alphabet $$\left\{ 0,1,...,k-1\right\} ^{n}$$ 0 , 1 , . . . , k - 1 n for some $$k\ge 2$$ k ≥ 2 . The set of k -FA-recognizable relations coincides with the set of relations, which are existentially definable in the structure "Image missing" , where "Image missing" corresponds to the bitwise minimum of base k . In order to obtain an existential first-order description of k -Parikh automata languages, we extend this structure with the predicate $$ EqNZB _{k}(x,y)$$ E q N Z B k ( x , y ) which is true if and only if x and y have the same number of non-zero bits in k -ary encoding. Using essentially the same ideas, we encode computations of k -multi-counter machines and thus show that every recursively enumerable relation over the natural numbers is existentially definable in the aforementioned structure supplemented with concatenation $$z=x\smallfrown _{k} y\rightleftharpoons z = x + k^{l_{k}(x)}y$$ z = x ⌢ k y ⇌ z = x + k l k ( x ) y , where $$l_{k}(x)$$ l k ( x ) is the bit-length of x in base k . This result gives us another proof of DPR-theorem.

We consider positively existentially definable sets in the structure {Ζ; 1, +,⊥}. It is well known that the elementary theory of this structure is undecidable while the existential theory is decidable. We show that after the extension of the signature with the unary '-' functional symbol, binary symbols for dis-equality ≠ and GCD (.,.)=d for every fixed positive integer d, every positive existential formula in this extended language is equivalent in Ζ to some positive quantifier-free formula.