An ILP-based Proof System for the Crossing Number Problem
An ILP-based Proof System for the Crossing Number Problem
复制标题
DOI：
10.4230/lipics.esa.2016.29
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Markus Chimani;Tilo Wiedera
中科院分区：
文献类型：
--
作者：
Markus Chimani;Tilo Wiedera
形式上，基于数学规划的方法能够找到可证明的最佳解决方案。然而，对可验证的形式证明的要求通常比我们可以合理地归因于数学程序实现的保证高得多。我们认为这是在上下文中的交叉数问题，拓扑图论中最突出的问题之一。这个问题要求在给定的图的任何绘图中的边交叉的最小数目。众所周知，这个问题的图论证明是非常难以获得的。与此同时，即使是非常特定的图的证明也经常在交叉数研究中引起兴趣，因为它们可以，例如，归纳证明的基础。我们提出了一个系统，自动生成一个正式的证明基于ILP计算。这样的证明是（相对）容易验证的，并且不需要理解任何复杂的ILP代码。因此，我们希望我们的证明系统可以作为一个展示的必要步骤和中心设计目标，如何建立基于数学规划公式的正式证明系统。
Formally, approaches based on mathematical programming are able to find provably optimal solutions. However, the demands on a verifiable formal proof are typically much higher than the guarantees we can sensibly attribute to implementations of mathematical programs. We consider this in the context of the crossing number problem, one of the most prominent problems in topological graph theory. The problem asks for the minimum number of edge crossings in any drawing of a given graph. Graph-theoretic proofs for this problem are known to be notoriously hard to obtain. At the same time, proofs even for very specific graphs are often of interest in crossing number research, as they can, e.g., form the basis for inductive proofs. We propose a system to automatically generate a formal proof based on an ILP computation. Such a proof is (relatively) easily verifiable, and does not require the understanding of any complex ILP codes. As such, we hope our proof system may serve as a showcase for the necessary steps and central design goals of how to establish formal proof systems based on mathematical programming formulations.