eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-08-18
29:1
29:13
10.4230/LIPIcs.ESA.2016.29
article
An ILP-based Proof System for the Crossing Number Problem
Chimani, Markus
Wiedera, Tilo
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol057-esa2016/LIPIcs.ESA.2016.29/LIPIcs.ESA.2016.29.pdf
automatic formal proof
crossing number
integer linear programming