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