Novel constraint synthesis methods for integer programs

整数规划是一种广泛应用的数学建模技术，它寻找线性不等式系统的积分解。标准的整数规划基准套件MIPLIB包括调度（学术时间表、火车、航空机组、护士/医生名册）、计算系统生物学、水系统规划、车辆路线和统计披露控制等应用程序。整数规划模型由复杂的求解器处理，主要基于分支定界和称为切割平面的约束的增量添加。许多感兴趣的问题仍然遥不可及：在撰写本文时，1065个MIPLIB集合中有286个尚未解决。在本建议中，在约束综合的保护伞下探索了求解和建模（即构造约束集）整数规划的新技术，即从高级输入生成约束。所提出的技术有望将现有解决方案的范围扩展到新的问题类别。对于某些问题，如果在这个集合上解决问题与考虑整个搜索空间得到相同的答案，那么一组候选点被称为核心集（或核心点集）。最近，一些作者开发了基于输入对称性的求解整数程序的核心集方法；当输入的重新标注产生等价的问题结构时，实际中就会出现问题对称性。这种等价的问题结构导致分支求解器的重复工作，而最先进的商业和研究求解器正在努力以各种方式打破这种对称性。而不是把对称性视为一个问题，核心技术寻求利用它来更快地解决整数程序。在最直接的方法中，核心要点被逐一列举和测试。目前对整数规划核心点问题的研究主要集中在核心点数目（或等价类数目）的边界问题上。我建议探索一种基于外部近似的新方法，特别是基于描述核心点集的约束的综合。这有可能使新的整数程序类可解，并且求解器作者和实践者（即需要求解整数程序的人）都感兴趣。虽然整数规划是一种非常通用的问题解决方法，但为求解器建模或构造输入的过程可能具有挑战性，并且实例的可跟踪性可能取决于建模者的技能（和运气）。我建议开发一个编译器，从可行点的简单程序描述中综合约束。根据最近在扩展公式方面的工作，这代表了直接生成约束的标准过程方法的一种对偶。我们计划将新的建模工具集成到现有的代数（声明性）建模语言中，使其能够以求解器独立的方式提供给实践者。

Integer Programming is a broadly applicable mathematical modelling technique that looks for integral solutions to systems of linear inequalities. The standard integer programming benchmark suite MIPLIB includes applications from scheduling (academic timetables, trains, airline crews, nurse/doctor rostering), computational systems biology, water system planning, vehicle routing, and statistical disclosure control. Integer programming models are processed by sophisticated solvers, primarily based on branch-and-bound and the incremental addition of constraints called cutting planes. Many problems of interest remain out of reach: 286 of the 1065 MIPLIB collection are unsolved as of this writing. In this proposal new techniques for solving and modelling (i.e. constructing sets of constraints for) integer programs are explored under the umbrella of constraint synthesis i.e. generating constraints from high level input. The proposed techniques promise to extend the reach of existing solvers to new problem classes. A set of candidates is called a coreset (or set of core points) for some problem if solving the problem on this set gives the same answer as considering the entire search space. Recently several authors have developed coreset methods for solving integer programs based on input symmetry; problem symmetries occur in practice when relabellings of the input yield equivalent problem structure. This equivalent problem structure causes repeated work for branching solvers, and state of the art commercial and research solvers make efforts to break the symmetries in various ways. Instead of seeing symmetry as a problem, coreset techniques seek to exploit it to solve integer programs faster. In the most direct approach, core points are enumerated and tested individually. Current research on core points for integer programming is mainly focused on bounding the number core points (or the number of equivalence classes). I propose to explore a new approach based on outer approximation, in particular based on the synthesis of constraints that describe the set of core points. This has the potential to make new classes of integer programs solvable, and is of interest to both solver writers and practitioners (i.e. people with integer programs to solve). While integer programming is a very general problem solving method, the process of modelling, or constructing input for a solver can be challenging, and the tractability of an instance can depend on the skill (and luck) of the modeller. I propose to develop a compiler to synthesize constraints from a simple procedural description of the feasible points. Based on recent work in extended formulations, this represents a kind of dual to the standard procedural approach of generating the constraints directly. We plan to integrate the new modelling tool into an existing algebraic (declarative) modelling language to make it available to practitioners in a solver independent way.