IntSat：基于冲突驱动约束学习的整数线性规划求解方法
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning
AI总结：
本文将 SAT 求解中的冲突驱动子句学习技术扩展到整数线性规划，提出 IntSat 方法并给出基础实现，证明其可作为现有 ILP 求解器的有效补充。
摘要：
当前最先进的 SAT 求解器已经能够处理大规模现实世界实例。其成功的关键在于所谓的冲突驱动子句学习（CDCL）方案，该方案包含一系列利用求解过程中所遇到冲突的技术。本文将上述技术扩展到整数线性规划（ILP）中，其中变量可以取一般整数值而非仅限二值，约束比单纯的命题子句更具表达力，并且可能存在需要优化的目标函数。我们解释了如何高效地实现这些方法，并讨论了可能的改进方向。我们的工作得到了一个基础实现的支持，该实现表明，即使在这一远未成熟的阶段，我们的技术也已经成为对当前 ILP 求解最先进方法的有益补充。
英文摘要：
State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the so-called Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the conflicts that are encountered during the search for a solution. In this article we extend these techniques to Integer Linear Programming (ILP), where variables may take general integer values instead of purely binary ones, constraints are more expressive than just propositional clauses, and there may be an objective function to optimise. We explain how these methods can be implemented efficiently, and discuss possible improvements. Our work is backed with a basic implementation that shows that, even in this far less mature stage, our techniques are already a useful complement to the state of the art in ILP solving.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
