Chimani, Markus ;
Wiedera, Tilo
An ILPbased Proof System for the Crossing Number Problem
Abstract
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. Graphtheoretic 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.
BibTeX  Entry
@InProceedings{chimani_et_al:LIPIcs:2016:6380,
author = {Markus Chimani and Tilo Wiedera},
title = {{An ILPbased Proof System for the Crossing Number Problem}},
booktitle = {24th Annual European Symposium on Algorithms (ESA 2016)},
pages = {29:129:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770156},
ISSN = {18688969},
year = {2016},
volume = {57},
editor = {Piotr Sankowski and Christos Zaroliagis},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6380},
URN = {urn:nbn:de:0030drops63803},
doi = {10.4230/LIPIcs.ESA.2016.29},
annote = {Keywords: automatic formal proof, crossing number, integer linear programming}
}
18.08.2016
Keywords: 

automatic formal proof, crossing number, integer linear programming 
Seminar: 

24th Annual European Symposium on Algorithms (ESA 2016)

Issue date: 

2016 
Date of publication: 

18.08.2016 