License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ESA.2016.29
URN: urn:nbn:de:0030-drops-63803
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6380/
Go to the corresponding LIPIcs Volume Portal

Chimani, Markus ; Wiedera, Tilo

An ILP-based Proof System for the Crossing Number Problem

pdf-format:
LIPIcs-ESA-2016-29.pdf (0.5 MB)

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. 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.

BibTeX - Entry

@InProceedings{chimani_et_al:LIPIcs:2016:6380,
  author =	{Markus Chimani and Tilo Wiedera},
  title =	{{An ILP-based Proof System for the Crossing Number Problem}},
  booktitle =	{24th Annual European Symposium on Algorithms (ESA 2016)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-015-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{57},
  editor =	{Piotr Sankowski and Christos Zaroliagis},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6380},
  URN =		{urn:nbn:de:0030-drops-63803},
  doi =		{10.4230/LIPIcs.ESA.2016.29},
  annote =	{Keywords: automatic formal proof, crossing number, integer linear programming}
}

Keywords: automatic formal proof, crossing number, integer linear programming
Collection: 24th Annual European Symposium on Algorithms (ESA 2016)
Issue Date: 2016
Date of publication: 18.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI