Document Open Access Logo

SAT Encoding of Partial Ordering Models for Graph Coloring Problems

Authors Daniel Faber, Adalat Jabrayilov , Petra Mutzel

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.12.pdf
  • Filesize: 0.85 MB
  • 20 pages

Document Identifiers

Author Details

Daniel Faber
  • Department of Computer Science, University of Bonn, Germany
Adalat Jabrayilov
  • Adesso SE, Dortmund, Germany
Petra Mutzel
  • Department of Computer Science, University of Bonn, Germany

Funding

  • Faber, Daniel: funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – 459420781.
  • Mutzel, Petra: This work has been funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) project no. 459420781 and under Germany’s Excellence Strategy–EXC-2047/1–390685813, and by the Federal Ministry of Education and Research of Germany and the state of North-Rhine Westphalia as part of the Lamarr-Institute for Machine Learning and Artificial Intelligence, LAMARR22B.

Acknowledgements

We are grateful for the valuable remarks of the referees, which helped to improve the paper.

Cite AsGet BibTex

Daniel Faber, Adalat Jabrayilov, and Petra Mutzel. SAT Encoding of Partial Ordering Models for Graph Coloring Problems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.12

Abstract

In this paper, we revisit SAT encodings of the partial-ordering based ILP model for the graph coloring problem (GCP) and suggest a generalization for the bandwidth coloring problem (BCP). The GCP asks for the minimum number of colors that can be assigned to the vertices of a given graph such that each two adjacent vertices get different colors. The BCP is a generalization, where each edge has a weight that enforces a minimal "distance" between the assigned colors, and the goal is to minimize the "largest" color used. For the widely studied GCP, we experimentally compare the partial-ordering based SAT encoding to the state-of-the-art approaches on the DIMACS benchmark set. Our evaluation confirms that this SAT encoding is effective for sparse graphs and even outperforms the state-of-the-art on some DIMACS instances. For the BCP, our theoretical analysis shows that the partial-ordering based SAT and ILP formulations have an asymptotically smaller size than that of the classical assignment-based model. Our practical evaluation confirms not only a dominance compared to the assignment-based encodings but also to the state-of-the-art approaches on a set of benchmark instances. Up to our knowledge, we have solved several open instances of the BCP from the literature for the first time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Mathematics of computing → Graph coloring
Keywords
  • Graph coloring
  • bandwidth coloring
  • SAT encodings
  • ILP formulations

Metrics

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

Related Versions

Supplementary Materials

References

  1. Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables into problems with boolean variables. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/53.pdf.
  2. Benchmarking machines and testing solutions. http://mat.gsia.cmu.edu/COLOR02/BENCHMARK/benchmark.tar, 2002.
  3. Gregory J. Chaitin, Marc A. Auslander, Ashok K. Chandra, John Cocke, Martin E. Hopkins, and Peter W. Markstein. Register allocation via coloring. Computer Languages, 6(1):47-57, 1981. URL: https://doi.org/10.1016/0096-0551(81)90048-5.
  4. Munmun Dey and Amitava Bagchi. Satisfiability methods for colouring graphs. In ACER 2013, volume 3, pages 135-147, March 2013. URL: https://doi.org/10.5121/csit.2013.3213.
  5. Bruno Dias, Rosiane De Freitas Rodrigues, Nelson Maculan, and Philippe Michelon. Integer and constraint programming approaches for providing optimality to the bandwidth multicoloring problem. RAIRO - Operations Research, 55:S1949-S1967, June 2021. URL: https://doi.org/10.1051/ro/2020065.
  6. Assefaw Hadish Gebremedhin, Fredrik Manne, and Alex Pothen. What color is your jacobian? Graph coloring for computing derivatives. SIAM Review, 47(4):629-705, 2005. URL: https://doi.org/10.1137/S0036144504444711.
  7. Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, and Nicolas Szczepanski. An incremental SAT-based approach to the graph colouring problem. In Thomas Schiex and Simon de Givry, editors, Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, volume 11802 of Lecture Notes in Computer Science, pages 213-231. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30048-7_13.
  8. Emmanuel Hebrard and George Katsirelos. Clause learning and new bounds for graph coloring. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19, pages 6166-6170, July 2019. URL: https://doi.org/10.24963/ijcai.2019/856.
  9. Emmanuel Hebrard and George Katsirelos. Constraint and satisfiability reasoning for graph coloring. J. Artif. Intell. Res., 69:33-65, 2020. URL: https://doi.org/10.1613/JAIR.1.11313.
  10. Stephan Held, William Cook, and Edward Sewell. Maximum-weight stable sets and safe lower bounds for graph coloring. Mathematical Programming Computation, 4, December 2012. URL: https://doi.org/10.1007/s12532-012-0042-3.
  11. Marijn J. H. Heule, Anthony Karahalios, and Willem-Jan van Hoeve. From Cliques to Colorings and Back Again. In Christine Solnon, editor, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022), volume 235 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:10, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2022.26.
  12. Thore Husfeldt. Graph colouring algorithms, 2015. URL: https://arxiv.org/abs/1505.05825.
  13. Adalat Jabrayilov and Petra Mutzel. New integer linear programming models for the vertex coloring problem. In Michael A. Bender, Martin Farach-Colton, and Miguel A. Mosteiro, editors, LATIN 2018: Theoretical Informatics - 13th Latin American Symposium, Buenos Aires, Argentina, April 16-19, 2018, Proceedings, volume 10807 of Lecture Notes in Computer Science, pages 640-652. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-77404-6_47.
  14. Adalat Jabrayilov and Petra Mutzel. Strengthened partial-ordering based ILP models for the vertex coloring problem. CoRR, abs/2206.13678, 2022. URL: https://doi.org/10.48550/arXiv.2206.13678.
  15. Frank Thomson Leighton. A graph coloring algorithm for large scheduling problems. Journal of research of the National Bureau of Standards, 84 6:489-506, 1979. URL: https://api.semanticscholar.org/CorpusID:16043293.
  16. Enrico Malaguti and Paolo Toth. A survey on vertex coloring problems. Int. Trans. Oper. Res., 17:1-34, 2010. URL: https://api.semanticscholar.org/CorpusID:9199689.
  17. Rafael Marti, Francisco Gortázar, and Abraham Duarte. Heuristics for the bandwidth colouring problem. Int. J. Metaheuristics, 1:11-29, January 2010. URL: https://doi.org/10.1504/IJMHEUR.2010.033121.
  18. Anuj Mehrotra and Michael A. Trick. A column generation approach for graph coloring. INFORMS J. Comput., 8:344-354, 1996. URL: https://api.semanticscholar.org/CorpusID:13978746.
  19. Isabel Méndez-Díaz and Paula Zabala. A cutting plane algorithm for graph coloring. Discrete Applied Mathematics, 156(2):159-179, 2008. Computational Methods for Graph Coloring and it’s Generalizations. URL: https://doi.org/10.1016/j.dam.2006.07.010.
  20. Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 11th, volume 3709 of Lecture Notes in Computer Science, pages 827-831. Springer, 2005. URL: https://doi.org/10.1007/11564751_73.
  21. Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear csp into sat. Constraints, 14(2):254-272, 2009. Google Scholar
  22. Michael Trick. DIMACS graph coloring instances. https://mat.tepper.cmu.edu/COLOR04/, 2002.
  23. Allen Van Gelder. Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics, 156(2):230-243, 2008. Computational Methods for Graph Coloring and it’s Generalizations. URL: https://doi.org/10.1016/j.dam.2006.07.016.
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 Imprint Privacy Contact