Orbit-finite linear programming

TL;DR

This paper introduces a decision procedure for solving linear programming problems with orbit-finite constraints over real numbers, extending classical LP to infinite, symmetric structures, but shows integer versions are undecidable.

Contribution

It provides the first decision procedure for orbit-finite linear programming over reals and demonstrates undecidability for the integer case.

Findings

Decidable for real solutions in orbit-finite LP

Undecidable for integer solutions in orbit-finite ILP

Extends classical linear programming to infinite symmetric structures

Abstract

An infinite set is orbit-finite if, up to permutations of the underlying structure of atoms, it has only finitely many elements. We study a generalisation of linear programming where constraints are expressed by an orbit-finite system of linear inequalities. As our principal contribution we provide a decision procedure for checking if such a system has a real solution, and for computing the minimal/maximal value of a linear objective function over the solution set. We also show undecidability of these problems in case when only integer solutions are considered. Therefore orbit-finite linear programming is decidable, while orbit-finite integer linear programming is not.