Document Open Access Logo

An ILP-based Proof System for the Crossing Number Problem

Authors Markus Chimani, Tilo Wiedera

PDF
Thumbnail PDF

File

LIPIcs.ESA.2016.29.pdf
  • Filesize: 467 kB
  • 13 pages

Document Identifiers

Author Details

Markus Chimani
Tilo Wiedera

Cite As Get BibTex

Markus Chimani and Tilo Wiedera. An ILP-based Proof System for the Crossing Number Problem. In 24th Annual European Symposium on Algorithms (ESA 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 57, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ESA.2016.29

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.

Subject Classification

Keywords
  • automatic formal proof
  • crossing number
  • integer linear programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. David Applegate, Robert E. Bixby, Vasek Chvátal, William J. Cook, Daniel G. Espinoza, Marcos Goycoolea, and Keld Helsgaun. Certification of an optimal TSP tour through 85, 900 cities. Oper. Res. Lett., 37(1):11-15, 2009. URL: http://dx.doi.org/10.1016/j.orl.2008.09.006.
  2. David Applegate, William J. Cook, Sanjeeb Dash, and Daniel G. Espinoza. Exact solutions to linear programming problems. Oper. Res. Lett., 35(6):693-699, 2007. URL: http://dx.doi.org/10.1016/j.orl.2006.12.010.
  3. Drago Bokal. On the crossing numbers of cartesian products with paths. Journal of Combinatorial Theory, Series B, 97(3):381-384, 2007. URL: http://dx.doi.org/10.1016/j.jctb.2006.06.003.
  4. Christoph Buchheim, Markus Chimani, Dietmar Ebner, Carsten Gutwenger, Michael Jünger, Gunnar W. Klau, Petra Mutzel, and René Weiskircher. A branch-and-cut approach to the crossing number problem. Discrete Optimization, 5(2):373-388, 2008. URL: http://dx.doi.org/10.1016/j.disopt.2007.05.006.
  5. Sergio Cabello. Hardness of approximation for crossing number. Discrete & Computational Geometry, 49(2):348-358, 2013. URL: http://dx.doi.org/10.1007/s00454-012-9440-6.
  6. Sergio Cabello and Bojan Mohar. Adding one edge to planar graphs makes crossing number and 1-planarity hard. SIAM Journal on Computing, 42:1803-1829, 2013. Google Scholar
  7. Markus Chimani. Computing Crossing Numbers. PhD thesis, TU Dortmund, 2008. URL: http://hdl.handle.net/2003/25955.
  8. Markus Chimani. Facets in the crossing number polytope. SIAM Journal on Discrete Mathematics, 25(1):95-111, 2011. URL: http://epubs.siam.org/sidma/resource/1/sjdmec/v25/i1/p95_s1, URL: http://dx.doi.org/10.1137/09076965X.
  9. Markus Chimani and Carsten Gutwenger. Non-planar core reduction of graphs. Discrete Mathematics, 309(7):1838-1855, 2009. URL: http://dx.doi.org/10.1016/j.disc.2007.12.078.
  10. Markus Chimani, Carsten Gutwenger, Michael Jünger, Gunnar W. Klau, Karsten Klein, and Petra Mutzel. The open graph drawing framework (OGDF). In Roberto Tamassia, editor, Handbook on Graph Drawing and Visualization., pages 543-569. Chapman &Hall/CRC, 2013. Google Scholar
  11. Markus Chimani, Carsten Gutwenger, and Petra Mutzel. Experiments on exact crossing minimization using column generation. ACM J. Experim. Alg., 14:4:3.4-4:3.18, 2010. URL: http://dx.doi.org/10.1145/1498698.1564504.
  12. Markus Chimani, Petra Mutzel, and Immanuel Bomze. A new approach to exact crossing minimization. In Proc. ESA, volume 5193 of LNCS, pages 284-296, 2008. URL: http://dx.doi.org/10.1007/978-3-540-87744-8_24.
  13. Marcel Dhiflaoui, Stefan Funke, Carsten Kwappik, Kurt Mehlhorn, Michael Seel, Elmar Schömer, Ralph Schulte, and Dennis Weber. Certifying and repairing solutions to large LPs how good are LP-solvers? In Proc. Fourteenth SODA, pages 255-256. ACM/SIAM, 2003. Google Scholar
  14. Giuseppe Di Battista, Ashim Garg, Giuseppe Liotta, Roberto Tamassia, Emanuele Tassinari, and Francesco Vargiu. An experimental comparison of four graph drawing algorithms. Computational Geometry, 7(5–6):303-325, 1997. 11th ACM Symposium on Computational Geometry. URL: http://dx.doi.org/10.1016/S0925-7721(96)00005-3.
  15. Guiseppe Di Battista, Ashim Garg, Guiseppe Liotta, Armando Parise, Roberto Tassinari, Emanuele Tassinari, Francesco Vargiu, and Luca Vismara. Drawing directed acyclic graphs: An experimental study. International Journal of Computational Geometry &Applications, 10(06):623-648, 2000. URL: http://dx.doi.org/10.1142/S0218195900000358.
  16. Geoffrey Exoo, Frank Harary, and Jerald Kabell. The crossing numbers of some generalized petersen graphs. Mathematica Scandinavica, 48(1):184-188, 1981. Google Scholar
  17. M. R. Garey and D. S. Johnson. Crossing number is NP-complete. SIAM Journal on Algebraic Discrete Methods, 4(3):312-316, 1983. URL: http://dx.doi.org/10.1137/0604033.
  18. Petr Hliněný. Crossing number is hard for cubic graphs. Journal of Combinatorial Theory. Series B, 96(4):455-471, 2006. URL: http://dx.doi.org/10.1016/j.jctb.2005.09.009.
  19. Michael Jünger and Stefan Thienel. The ABACUS system for branch-and-cut-and-price algorithms in integer programming and combinatorial optimization. Softw., Pract. Exper., 30(11):1325-1352, 2000. URL: http://dx.doi.org/10.1002/1097-024X(200009)30:11<1325::AID-SPE342>3.0.CO;2-T.
  20. Ken-ichi Kawarabayashi and Buce Reed. Computing crossing number in linear time. In Proc. STOC, pages 382-390, 2007. URL: http://dx.doi.org/10.1145/1250790.1250848.
  21. Marián Klešč. The crossing numbers of join of the special graph on six vertices with path and cycle. Discrete Math., 310(9):1475-1481, 2010. URL: http://dx.doi.org/10.1016/j.disc.2009.08.018.
  22. Marián Klešč, R. Bruce Richter, and Ian Stobert. The crossing number of C₅ × C_n. Journal of Graph Theory, 22(3):239-243, 1996. URL: http://dx.doi.org/10.1002/(SICI)1097-0118(199607)22:3<239::AID-JGT4>3.0.CO;2-N.
  23. Jan Kratochvíl. String graphs. II. recognizing string graphs is NP-hard. Journal of Combinatorial Theory, Series B, 52(1):67-78, 1991. URL: http://dx.doi.org/10.1016/0095-8956(91)90091-W.
  24. Casimir Kuratowski. Sur le problème des courbes gauches en topologie. Fundamenta Mathematicae, 15(1):271-283, 1930. URL: http://eudml.org/doc/212352.
  25. Dan McQuillan, Shengjun Pan, and R. Bruce Richter. On the crossing number of K_13. Journal of Combinatorial Theory, Series B, 115:224-235, 2015. URL: http://dx.doi.org/10.1016/j.jctb.2015.06.002.
  26. Dan McQuillan and R. Bruce Richter. On the crossing numbers of certain generalized petersen graphs. Discrete Mathematics, 104(3):311-320, 1992. URL: http://dx.doi.org/10.1016/0012-365X(92)90453-M.
  27. Lars Noschinski, Christine Rizkallah, and Kurt Mehlhorn. Verification of certifying computations through autocorres and simpl. In Proc. NASA Formal Methods - 6th International Symposium, volume 8430 of LNCS, pages 46-61, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06200-6_4.
  28. Shengjun Pan and R. Bruce Richter. The crossing number of K_11 is 100. Journal of Graph Theory, 56(2):128-134, 2007. URL: http://dx.doi.org/10.1002/jgt.v56:2.
  29. Marcus Schaefer. The graph crossing number and its variants: a survey. Electronic Journal of Combinatorics, 2013. Google Scholar
  30. Imrich Vrt’o. Crossing numbers of graphs: A bibliography. ftp://ftp.ifi.savba.sk/pub/imrich/crobib.pdf, 2014.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact