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.
翻译:如果一个无限集在底层原子结构的置换下仅有有限个元素,则称该集合为轨道有限的。我们研究了一种线性规划的推广形式,其中约束条件由轨道有限的线性不等式系统表达。作为主要贡献,我们提出了一种判定过程,用于检验此类系统是否存在实数解,并计算线性目标函数在解集上的最小/最大值。我们还证明了当仅考虑整数解时,这些问题是不可判定的。因此,轨道有限线性规划是可判定的,而轨道有限整数线性规划则不可判定。