24
$\begingroup$

It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, multiplication, and the constant $1$), with free variables taking values in the integers, deciding whether the formula is satisfiable is undecidable.

If multiplication $\cdot$ is replaced by the binary greatest-common-divisor (gcd) function, defined appropriately for 0 and negative numbers, does the satisfiability problem remain undecidable?

For example, the input might be a formula like $$ a + b = c \land \gcd(a, b) = 2 \land \gcd(a, c) = 1 $$ or $$ \gcd(a, \gcd(b, c) + b) = a + c \land \lnot (\gcd(a, b) = a). $$

I suspect this to be a basic result in the study of decidability results for integer theories, but this came up in another context and I am not entirely familiar. From a brief literature search (see On Decidability Within the Arithmetic of Addition and Divisibility, Marius Bozga and Radu Iosif) I know of the following classical results:

  • The theory of $\{=, +, |\}$ (where $|$ is divisibility) allowing quantifiers is undecidable (Julia Robinson 1949).

  • The satisfiability of quantifier-free formulas over $\{=, +, |\}$ (i.e. existential fragment of the above) is decidable. (The diophantine problem for addition and divisibility, Leonard Lipshitz 1976.)

Divisibility can be defined in terms of gcd ($a \mid b \iff \gcd(a, b) = a$), but vice versa requires existential quantification ($\gcd(a, b) = c \iff (c \mid a) \land (c \mid b) \land \exists x \exists y.\; c = ax + by$), which won't work in quantifier-free formulas in a negated context, so at least at first glance I am not sure that gcd is equivalent to divisibility for the purposes of decidability.

Improve this question
$\endgroup$
3
  • $\begingroup$ It came up in another context -- decidability of fragments of regular expressions can be studied by starting from regular expressions over a unary alphabet, and looking at the subsets of integer constraints that can be encoded. One such fragment gave rise to roughly this theory. $\endgroup$ Commented Dec 27, 2020 at 5:59
  • $\begingroup$ Thanks! As to the original problem I am afraid I can't be more precise, I hadn't formulated everything myself clearly. There are different fragments corresponding to different integer theories and the correspondence is not so direct (for instance, for the original fragment of unary alphabet REs I was thinking of, I believe more can be expressed than just $\gcd$. But per your comments, remains undecidable). $\endgroup$ Commented Dec 27, 2020 at 6:07
  • 3
    $\begingroup$ Isn't $\mathrm{gcd}(a,b)\neq c$ the same as $(c\nmid a)\vee(c\nmid b)\vee(\exists d. (c|d)\wedge(c\neq \pm d)\wedge(d|a)\wedge(d|b))$? So it reduced to quantifier-free divisibility formulas no matter negated or not. $\endgroup$ Commented Dec 27, 2020 at 8:37

3 Answers 3

Reset to default
24
$\begingroup$

($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$, and $\le$: $$\begin{align*} \gcd(a,b)=c&\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\ &\iff c\ge0\land c\mid a\land c\mid b\land\exists u,v\:(a\mid u\land b\mid v\land c=u+v). \end{align*}$$ Thus, any existential sentence over the structure $\langle\mathbb Z,+,\gcd\rangle$ (or even $\langle\mathbb Z,{\le},+,\gcd\rangle$) can be (in polynomial time) converted to an equivalent existential sentence over the structure $\langle\mathbb Z,{\le},+,|\rangle$, which can in turn be converted to an equivalent existential sentence over the structure $\langle\mathbb N,+,|\rangle$ in the obvious way. The last problem is decidable by the result of Lipshitz [1] quoted in the question.

Reference:

[1] Leonard Lipshitz: The Diophantine problem for addition and divisibility, Transactions of the American Mathematical Society 235 (1978), pp. 271–283, doi: 10.1090/S0002-9947-1978-0469886-1.

Improve this answer
$\endgroup$
9
  • 1
    $\begingroup$ Perfectly clear! Thank you for your answer. $\endgroup$ Commented Dec 27, 2020 at 16:30
  • 4
    $\begingroup$ This is all the more interesting because it would appear that using least common multiple (lcm) instead of gcd becomes undecidable. lcm can be used to encode squares via the trick $x^2 - 1 = \text{lcm}(x + 1, x - 1)$ (assuming $x$ even, with a similar constraint for $x$ odd), then squares can be used to encode multiplication. $\endgroup$ Commented Dec 27, 2020 at 20:07
  • 2
    $\begingroup$ Indeed, this is an interesting connection. lcm has a universal definition similar to gcd, but apparently not an existential definition. $\endgroup$ Commented Dec 27, 2020 at 20:40
  • $\begingroup$ @EmilJeřábek The paper quoted also states multiplication can be defined from $+,|$. So is any existential sentence over $\langle\mathbb Z,+,\times\rangle$ decidable? The paper states $\exists x_1,\dots,x_n\forall y\Delta(x_1,\dots,x_n,y)$ might be undecidable if $\Delta$ is an open formula. I do not know what an open formula means. $\endgroup$ Commented Dec 18, 2021 at 2:42
  • 2
    $\begingroup$ @Turbo (late reply) "is any existential sentence over ⟨ℤ,+,×⟩ decidable?" Certainly not as that is Hilbert's 10th problem. I didn't take another look at the paper but probably the definition of multiplication uses quantifiers. $\endgroup$ Commented Jul 18, 2024 at 17:46
10
$\begingroup$

A something that might be too long for a comment, based on the previous answer by Emil.

In the case you are interested in the complexity of such a logic, consider reading:

[1] On the Complexity of Linear Arithmetic with Divisibility, by Joël Ouaknine, Antonia Lechner and Ben Worrell. A preprint is available here: https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf

According to the authors, the proof by Lipshitz is of considerable mathematical depth and intricacy and is difficult to read and understand. So I hope that the attached paper will be more useful in this context. Note that the complexity of the existential fragment of Presburger arithmetic with divisibility is still open (NP-hard, in NEXP). Fortunately, replacing divisibility by a binary gcd predicate has been recently studied and the satisfiability problem is NP-complete.

[2] Integer Programming with GCD Constraints, by Rémy Défossez, Christoph Haase, Alessio Mansutti, and Guillermo A. Pérez. https://epubs.siam.org/doi/10.1137/1.9781611977912.128

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thank you for the interesting reference! $\endgroup$ Commented Dec 27, 2020 at 16:31
  • $\begingroup$ Yes, thank you for the reference. Is there other related material you can recommend? $\endgroup$ Commented Dec 28, 2020 at 0:21
  • $\begingroup$ Not really, the only other thing that I know and can be related is Presburger Arithmetics + Modulo Counting, here: link.springer.com/chapter/10.1007%2F978-3-662-46678-0_24 $\endgroup$ Commented Dec 28, 2020 at 8:53
0
$\begingroup$

Revisiting this just to post a comment on the post and on @Emil Jeřábek's excellent answer. In fact, only the existential definition is needed, not the universal definition, exploiting the fact that gcd is a function. Namely, considering the satisfiability of any formula $\phi$ over gcd, say in DNF, and supposing we have a clause $$ \phi \land \lnot (\gcd(a, b) = c) $$ we can simply rewrite this as $$ \exists c'. \phi \land (\gcd(a, b) = c') \land \lnot (c = c'). $$ Hence, applying the existential encoding to the former clause from Emil's answer, that is $$ \gcd(a,b)=c' \iff c'\ge0\land c'\mid a\land c'\mid b\land\exists u,v\:(a\mid u\land b\mid v\land c'=u+v) $$ results in a purely existential formula equivalent to the original without the negated $\gcd$ constraint, and once this is done with all instances of gcd, we are left with a formula over $\{+, |\}$.

Of course, if we were interested only in the relation that c is a gcd of a and b (negative or positive) not the gcd, then we may need both the universal and existential definitions to make the reduction work. This issue can be eliminated by simply defining the functional (positive) version from the relational one.

Improve this answer
$\endgroup$
2
  • $\begingroup$ "a gcd" Did you mean just a common divisor? There can be only one gcd. Also, if you don't require it to be the greatest, then the statement like $cd(a,b)=c$ does not make sense, you need it to be like $\exists c.c>1\land cd(a,b)=c$. $\endgroup$ Commented May 2, 2025 at 0:18
  • $\begingroup$ @rus9384 The aside comment may not be that useful. I meant, since if allowing negatives there are two gcds (a negative one and a positive one). In this case, gcd is a relation and the reduction does not directly apply. Of course the relation becomes functional with a single added constraint so it is trivial to convert the relation into a function. $\endgroup$ Commented May 2, 2025 at 1:34

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.