Publication
Title
Integer programming with GCD constraints
Author
Abstract
We study the non-linear extension of integer programming with greatest common divisor constraints of the form gcd(f, g) ~ d, where f and g are linear polynomials, d is a positive integer, and ~ is a relation among ≤, = ≠, = and ≥. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it exists, has polynomial bit length. To show these results, we identify an expressive fragment of the existential theory of the integers with addition and divisibility that admits solutions of polynomial bit length. It was shown by Lipshitz [Trans. Am. Math. Soc., 235, pp. 271-283, 1978] that this theory adheres to a local-to-global principle in the following sense: a formula Φ is equi-satisfiable with a formula Ψ in this theory such that Ψ has a solution if and only if Ψ has a solution modulo every prime p. We show that in our fragment, only a polynomial number of primes of polynomial bit length need to be considered, and that the solutions modulo prime numbers can be combined to yield a solution to Φ of polynomial bit length. As a technical by-product, we establish a Chinese-remainder-type theorem for systems of congruences and non-congruences showing that solution sizes do not depend on the magnitude of the moduli of non-congruences.
Language
English
Source (book)
Proceedings of the 2024 ACM-SIAM Symposium on Discrete Algorithms (SODA)
Publication
2024
ISBN
978-1-61197-791-2
DOI
10.1137/1.9781611977912.128
Volume/pages
p. 3605-3658
Full text (Publisher's DOI)
Full text (open access)
Full text (publisher's version - intranet only)
UAntwerpen
Faculty/Department
Research group
Project info
SAILor: Safe Artificial Intelligence and Learning for Verification.
Publication type
Subject
Affiliation
Publications with a UAntwerp address
External links
Record
Identifier
Creation 10.04.2024
Last edited 12.04.2024
To cite this reference