Novel constraint synthesis methods for integer programs

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

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.