Algorithms for Short Human-Verifiable Proofs of Non-Word-Representability

Abstract

A graph is word-representable if it can be represented using alternation of letters in words. The class of word-representable graphs generalizes several important graph families and admits a characterization via semi-transitive orientations. Recognizing word-representability is an NP-complete problem, and a major bottleneck in the theory of word-representable graphs is providing efficient justifications of non-word-representability of graphs, rather than merely referring to software verification. Recently, Kitaev and Sun initiated the development of methods for the automatic generation of human-verifiable proofs of non-word-representability. They introduced three algorithms and evaluated their performance on the 25 connected non-word-representable graphs on seven vertices, which constitute a fairly small sample set. In this paper, we confirm their ranking of the algorithms by testing them on all non-word-representable graphs on eight and nine vertices. We further introduce three new algorithms, one of which significantly outperforms the previously best method on graphs with at most nine vertices, producing substantially shorter proofs. We apply this algorithm to shorten a known proof of non-word-representability of the Shrikhande graph and to produce a proof of non-word-representability of a certain subgraph of the Kneser graph $K(8,3)$. This subgraph is the first known example of a triangle-free non-word-representable graph, presented in the literature with reference only to a computational proof. As a by-product of our study, we correct an error in the repeatedly published list of the 25 connected non-word-representable graphs on seven vertices.