Recognizing Chordal Graphs: Lex BFS and MCS¹

We are formalizing the algorithm for recognizing chordal graphs by lexicographic breadth-first search as presented in [13, Section 3 of Chapter 4, pp. 81-84]. Then we follow with a formalization of another algorithm serving the same end but based on maximum cardinality search as presented by Tarjan and Yannakakis [25].

This work is a part of the MSc work of the first author under supervision of the second author. We would like to thank one of the anonymous reviewers for very useful suggestions.