DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.7

On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Authors: Piotr Bacik, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, Madhavan Venkatesh, and Emil Rugaard Wieser

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n³-5n+3, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.

Cite as

Piotr Bacik, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, Madhavan Venkatesh, and Emil Rugaard Wieser. On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacik_et_al:LIPIcs.LICS.2026.7,
  author =	{Bacik, Piotr and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Vahanwala, Mihir and Venkatesh, Madhavan and Wieser, Emil Rugaard},
  title =	{{On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.7},
  URN =		{urn:nbn:de:0030-drops-267947},
  doi =		{10.4230/LIPIcs.LICS.2026.7},
  annote =	{Keywords: Presburger arithmetic, Diophantine equations, decidability, B\"{u}chi’s conjecture}
}

Document

DOI: 10.4230/LIPIcs.LICS.2026.8

On the Subspace Orbit Problem and the Simultaneous Skolem Problem

Authors: Piotr Bacik and Anton Varonka

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomial time by Kannan and Lipton. This decidability result was later extended by Chonev et al. to targets of dimension 3 (in arbitrary ambient dimension), but decidability remains open for subspaces of dimension 4. At the other extreme, the special case of the Orbit Problem in which the target set is a hyperplane of co-dimension 1 is equivalent to the Skolem Problem for linear recurrence sequences, whose decidability has been open for many decades. In this paper, we show that the Orbit Problem is decidable if the target subspace has dimension logarithmic in the dimension of the orbit. Over the rationals, we moreover obtain a complexity bound NP^RP in this case, when the target space dimension is bounded. On the other hand, we show that the version of the Orbit Problem where the dimension of the target subspace is linear in the dimension of the orbit is as hard as the Skolem Problem.

Cite as

Piotr Bacik and Anton Varonka. On the Subspace Orbit Problem and the Simultaneous Skolem Problem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 8:1-8:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacik_et_al:LIPIcs.LICS.2026.8,
  author =	{Bacik, Piotr and Varonka, Anton},
  title =	{{On the Subspace Orbit Problem and the Simultaneous Skolem Problem}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{8:1--8:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.8},
  URN =		{urn:nbn:de:0030-drops-267955},
  doi =		{10.4230/LIPIcs.LICS.2026.8},
  annote =	{Keywords: Orbit Problem, Skolem Problem, Simultaneous Skolem Problem, Linear Recurrence Sequences, Verification}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.8

On the p-adic Skolem Problem

Authors: Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many p-adic zeros. In this paper we consider the problem of determining whether a given LRS has a p-adic zero, as well as the corresponding function problem of computing exact representations of all p-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the p-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the p-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the p-adic Schanuel Conjecture.

Cite as

Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell. On the p-adic Skolem Problem. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacik_et_al:LIPIcs.STACS.2026.8,
  author =	{Bacik, Piotr and Ouaknine, Jo\"{e}l and Purser, David and Worrell, James},
  title =	{{On the p-adic Skolem Problem}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.8},
  URN =		{urn:nbn:de:0030-drops-254979},
  doi =		{10.4230/LIPIcs.STACS.2026.8},
  annote =	{Keywords: Skolem Problem, p-adic Schanuel Conjecture, Skolem Conjecture, Exponential Local-Global Principle, exponential polynomial}
}

Search Results

Documents authored by Bacik, Piotr

On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Abstract

Cite as

On the Subspace Orbit Problem and the Simultaneous Skolem Problem

Abstract

Cite as

On the p-adic Skolem Problem

Abstract

Cite as

Thanks for your feedback!

Could not send message