An ILP-based proof system for the crossing number problem
Autor(en): | Chimani, M. Wiedera, T. |
Herausgeber: | Zaroliagis, C. Sankowski, P. |
Stichwörter: | Automatic formal proof; Computation theory; Crossing number; Edge crossing; Formal proofs; Graph theory; Graph-theoretic; Integer linear programming; Mathematical program; Mathematical programming; Optimal solutions; Programmable logic controllers; Topological graph theories, Integer programming; Topology, Crossing number | Erscheinungsdatum: | 2016 | Herausgeber: | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing | Journal: | Leibniz International Proceedings in Informatics, LIPIcs | Volumen: | 57 | Zusammenfassung: | 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. © Markus Chimani and Tilo Wiedera. |
Beschreibung: | Conference of 24th Annual European Symposium on Algorithms, ESA 2016 ; Conference Date: 22 August 2016 Through 24 August 2016; Conference Code:123447 |
ISBN: | 9783959770156 | ISSN: | 18688969 | DOI: | 10.4230/LIPIcs.ESA.2016.29 | Externe URL: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85012963408&doi=10.4230%2fLIPIcs.ESA.2016.29&partnerID=40&md5=e239ab77841774a8b30c9b800e2e40a0 |
Zur Langanzeige
Seitenaufrufe
5
Letzte Woche
0
0
Letzter Monat
0
0
geprüft am 03.06.2024