2026-07-25T02:34:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22190 2024-12-05T15:18:03Z ddc:004 open_access

An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper) Chistikov, Dmitry Logical theories of arithmetic decision procedures Presburger arithmetic, or linear integer arithmetic (LIA), is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by nonzero n ∈ ℤ. More formally, it is the first-order theory of integers with addition and ordering. This paper offers a short introduction: what can be expressed in this logical theory, decision problems, and automated reasoning methods. We begin with an elementary introduction, explaining the language of linear arithmetic constraints by examples. We adopt a theoretical perspective, focusing on the decision problem: determining the truth value of a logical sentence. The following three views on Presburger arithmetic give us three effective methods for decision procedures: a view from geometry (using semi-linear sets), from automata theory (using finite automata and recognizable sets), and from symbolic computation (using quantifier elimination). The decision problem for existential formulas of Presburger arithmetic is essentially the feasibility problem of integer linear programming. By a fundamental result due to Borosh and Treybig [Proc. Am. Math. Soc. 55(2), 1976] and Papadimitriou [J. ACM 28(4), 1981], it belongs to the complexity class NP. Echoing the three views discussed above, we sketch three proofs of this result and discuss how these ideas have been used and developed in the recent research literature. This is a companion paper for a conference talk focused on the three views on Presburger arithmetic and their applications. The reader will require background knowledge at the level of undergraduate computer science curricula. The discussion of complexity aspects is more advanced. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dmitry Chistikov 2024 Is Part Of LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2024.1 urn:nbn:de:0030-drops-221909 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.1 eng https://creativecommons.org/licenses/by/4.0/legalcode