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

Introduction

There is an extensive body of literature devoted to the theory of word-representable graphs (see, e.g., [6, 7] and the references therein). The interest in this class stems from its connections to algebra, graph theory, computer science, combinatorics on words, and scheduling [7]. In particular, word-representable graphs generalize several fundamental graph classes, including circle graphs, 3-colorable graphs, and comparability graphs.

Two distinct letters $x$ and $y$ are said to alternate in a word $w$ if after deleting from $w$ all letters except $x$ and $y$ the resulting word is of the form $xyxy\cdots$ or $yxyx\cdots$, of either even or odd length. A graph $G=(V,E)$ is word-representable if and only if there exists a word $w$ over the alphabet $V$ such that, for distinct $x,y\in V$, the letters $x$ and $y$ alternate in $w$ if and only if $xy\in E$. In this case, we say that $w$ represents $G$. A graph is word-representable if and only if each of its connected components is word-representable [7]. Therefore, without loss of generality, we may restrict our attention to connected graphs.

The smallest non-word-representable graph (in terms of the number of vertices) has six vertices; it is the wheel graph $W_5$ (obtained from Graph 1 in Figure 4 by removing vertex 7). In contrast, there are 25 connected non-word-representable graphs on seven vertices [7]. The numbers of such graphs on eight to eleven vertices are 929, 54957, 4880093, and 650856040, respectively. This sequence took three years to compute and is listed as A290814 in the OEIS [13].

Vector (PDF)

An orientation of a graph is semi-transitive if it is acyclic (i.e., there are no directed cycles) and satisfies the following condition: for every directed path

either there is no edge between $v_0$ and $v_k$, or $v_i\to v_j$ is an edge for all $0\le i<j\le k$. An induced subgraph on vertices $\{v_0,v_1,\ldots,v_k\}$ of an oriented graph is a shortcut if its orientation is acyclic and non-transitive, and it contains both the directed path $v_0\to v_1\to\cdots\to v_k$ and the edge $v_0\to v_k$, which is referred to as the shortcutting edge. Equivalently, a semi-transitive orientation can be defined as an acyclic orientation containing no shortcuts. A fundamental result in the area is the following characterization.

The following known results are important for our paper.

Recognizing word-representability of a graph is NP-complete [7]. A major practical difficulty in the theory of word-representable graphs is providing convincing and efficient proofs of non-word-representability, particularly when references to software (even publicly available and user-friendly tools such as [2]) are undesirable. In contrast, word-representability can be certified by exhibiting a semi-transitive orientation, which can be verified in polynomial time [7].

Proving non-word-representability

A comparability graph is an undirected graph that admits a transitive orientation. It is known (see [8]) that the neighbourhood of every vertex in a word-representable graph is a comparability graph, and recognizing comparability graphs can be done in polynomial time [3]. Therefore, we obtain a polynomial-time test for non-word-representability of a graph $G$: for each vertex, verify whether its neighbourhood induces a comparability graph; if a neighbourhood that is not a comparability graph is found, then $G$ is not word-representable. On the other hand, if all neighbourhoods are comparability graphs, the test is inconclusive, as the graph may or may not be word-representable [7].

Thus, if the test above fails and no known non-word-representable induced subgraph is found in the given graph, then, prior to [11], the possible approaches to justify non-word-representability were the following:

• (a) To produce some kind of ad-hoc (preferably elegant) argument that assumes the existence of a semi-transitive orientation and derives a contradiction. This approach is preferable, but such arguments are usually difficult to construct.

• (b) To examine all $O(2^{\#\mathrm{edges}})$ orientations and justify that none of them is semi-transitive. Symmetries can be exploited to reduce the search space; in particular, any given edge may be assumed to have a fixed orientation. A variation of this approach is implemented in some existing software [2, 14]. It proceeds as follows: orient an edge $e_1$ in a given graph $G$, then select an as yet unoriented edge $e_2$ and branch on it, creating two copies of the partially oriented graph by orienting $e_2$ in the two possible ways; then branch on $e_3$, and so on. At each step, one ensures that no directed cycles or shortcuts are created (if they are, the corresponding branch is discarded). In any case, even if a computer were to output all these orientations (or the entire branching process) and indicate a directed cycle or a shortcut in each orientation, such a proof would be essentially unverifiable by a human, as it would typically be far too long.

(c) To examine all $O(\#\mathrm{vertices}^{2})$-length words in which each vertex label occurs the same number of times and to verify that none of them has the required alternation properties (if a graph with $n$ vertices is word-representable, then there exists a representing word of length at most $2n^{2}$ [5]). This approach requires checking a vast number of words. However, constraint programming can be used to speed up the process [15]. In either case, it is impossible to convincingly demonstrate non-word-representability in this way without referring to software.

(d) Simply refer to publicly available software [2, 14, 15], which is less desirable, but still a valid option.

A game-changing approach that significantly increases the variety of non-word-representable graphs for which we can justify non-word-representability in a human-verifiable way was suggested in [11] by Kitaev and Sun. The basic idea in [11] is to modify the branching process using Lemma 1, which helps avoid unnecessary branching through certain preprocessing steps. This modification enabled the development of software [14] that can automatically generate human-verifiable proofs of non-word-representability. The primary criterion for the efficiency of an algorithm is the number of “lines” (in the sense specified below) in the proof it produces; the secondary criterion is the running time of the algorithm. The latter is not discussed in this paper, as it is less relevant to our goals (the problem is NP-complete, and our focus is on proof length). In fact, the approach in [11] is not novel: several papers, including [9], use it or a simpler version of it (considering cycles of length 3 and 4 only) to justify non-word-representability. However, [11] is the first paper to discuss the automated search for human-verifiable proofs of non-word-representability of graphs, which led to the development of publicly available, user-friendly software [14].

Theorem 2 provides a further dramatic reduction in the size of proofs of non-word-representability and thereby further enlarges the class of non-word-representable graphs for which we can provide “short” proofs in a fully automatic manner. Indeed, selecting a vertex of maximum degree in a given non-word-representable graph, assuming it to be a source, and then running the branching process typically results in a much shorter proof. However, there are cases in which assuming a vertex of smaller degree to be a source leads to a shorter proof.

Our contributions

The paper [11] introduces three algorithms based on Lemma 1 to generate shorter proofs of non-word-representability. These algorithms were tested and ranked (by average performance) only on the 25 non-word-representable graphs on seven vertices, which is a rather small sample. We tested the algorithms on all non-word-representable graphs on eight and nine vertices and confirmed their ranking. Moreover, we propose three additional algorithms to address the problem, one of which significantly outperforms the best known algorithm so far, while the other two may be useful for particular graphs. In Section 2, we sketch all six algorithms and discuss their observed performance, and we provide pseudocode for the empirically best-performing one. We note that in our tests we chose not to use Theorem 2; employing this theorem and considering all possible assumptions about a source could lead to different results in the comparison of the algorithms.

The paper [11] used software [14] as a proof of concept to find automatically generated “short” proofs of non-word-representability for the Shrikhande graph on 16 vertices and 48 edges (see Figure 2), and the Clebsch graph on 16 vertices and 40 edges. The latter graph has the even-cardinality subsets of $\{1, 2, 3, 4, 5\}$ as vertices, with two subsets adjacent if and only if their symmetric difference has cardinality four. While our best-performing algorithm (on average) does not improve the length of the proof for the Clebsch graph, it reduces the proof length by one third for the Shrikhande graph. The publicly available software [17] can be used to confirm our results.

Vector (PDF)

For any two integers $k \ge1$ and $n \ge k$, the Kneser graph $K(n, k)$ is the graph whose vertices correspond to the $k$-element subsets of the set $\{1, 2, \ldots, n\}$, where two vertices are adjacent if and only if the corresponding sets are disjoint. Kneser graphs are vertex-transitive and edge-transitive, and they are named after Martin Kneser, who first investigated them in 1955. The subgraph $S$ of the Kneser graph $K(8,3)$ presented in [10] and displayed in Figure 3 is the first explicit example of a triangle-free non-word-representable graph; the existence of such graphs was established via Erdős’s theorem in [4]. A systematic study of the word-representability of triangle-free graphs was conducted in [9]. Unfortunately, the non-word-representability of $S$ was established in [10] only computationally (by referring to the software [2]). We are now in a position to provide a human-verifiable proof of the non-word-representability of $S$; see § 3 for further details.

Vector (PDF)

Finally, the list of all 25 connected non-word-representable graphs on seven vertices has been published multiple times, for example in [7]. The paper [11] corrected two graphs in the list. However, we observed that the list presented in [11] still contains one incorrect graph. This graph, called Graph 20 in [11], is the undirected version of the semi-transitively oriented graph shown in Figure 1. We leave it to the reader as a straightforward exercise to verify that the orientation in Figure 1 is indeed semi-transitive. The correct list of the 25 connected non-word-representable graphs on seven vertices can be found in Figure 4, and a proof of non-word-representability of the updated Graph 20 follows from the easy-to-check fact that the neighborhood of vertex 1 is not a comparability graph. A proof for this graph, viewed as the line graph of the triangular book

Vector (PDF)

graph with three pages, is also given in [12 Lemma 10].

Six algorithms for producing proofs

In this section, we describe three known algorithms and three new algorithms for finding proofs of non-word-representability of graphs. All of these algorithms rely on the observation that the branching process should not involve any edges that do not belong to a cycle, since such edges can be oriented arbitrarily without affecting the semi-transitivity of the rest of the graph’s orientation. Moreover, all three algorithms assume that, to produce a shorter proof, branching should be performed on edges that belong to many cycles, which tends to increase the number of applications of Lemma 1. In any case, we begin by explaining the format of a proof of non-word-representability of a graph and give a small example below; see also [11]. A completed exhaustive search is conclusive: either all branches close, proving non-word-representability, or a surviving terminal partial orientation can be completed semi-transitively. At such a terminal state, all edges belonging to non-clique cycles are already oriented. Orienting the remaining edges according to a topological ordering preserves acyclicity and cannot create a shortcut, since the path and shortcutting edge of any shortcut form a non-clique cycle. A search stopped before either outcome is established is inconclusive.

We write $uv$ for the undirected edge $\{u,v\}$ and $u \to v$ for an assigned direction. For lexicographic comparisons, vertex labels are ordered numerically and each edge $uv$ is represented by the pair $(u,v)$ with $u < v$, irrespective of any assigned direction. A cycle is represented by the lexicographically smallest vertex sequence among its cyclic shifts and their reversals.

The format of a proof

By a “line” of a proof, we mean a sequence of instructions that directs the orientation of a partially oriented graph and necessarily ends with a contradiction showing that this particular orientation branch will not produce a semi-transitive orientation. The idea is that if no branch produces a semi-transitive orientation, then the graph is not word-representable.

Each proof begins with assumptions on the orientations of certain edges, and there are four types of instructions:

• “B$a \to b$ (Copy $x$)” means “Branch on edge $ab$, orient the edge as $a \to b$, create a copy of the current version of the graph with the edge $ab$ oriented as $b \to a$, and call the new copy $x$; leave Copy $x$ aside and continue to follow the instructions.” The instruction B occurs when no application of Lemma 1 is possible in the partially oriented graph.

• “MC$x$” means “Move to Copy $x$,” where Copy $x$ is a partially oriented version of the graph created at some point in the branching process. This

instruction is always followed by an oriented edge $a \to b$ to remind the reader of the directed edge obtained after branching.

• “$Oa \to b (Cabc)$” means orient the edge $ab$ as $a \to b$ in the cycle $abc$ to avoid a directed cycle. If the cycle is longer than a triangle, this represents an application of Lemma 1 to produce a cycle where all but two edges are oriented in one direction, and one of the remaining two edges is oriented in the opposite direction.

• “$Oa \to b \; Oc \to d (Cxyz \cdots)$” means that Lemma 1 is applied to cycle $xyz \cdots$ to create new directed edges $a \to b$ and $c \to d$.

Each line ends with either “S: $x$-$y$-$\cdots$-$z$,” indicating a shortcut with directed path $x \to y \to\cdots\to z$ and shortcutting edge $x \to z$, or “E: $x$-$y$-$\cdots$-$z$,” indicating an orientation contradiction on the displayed cycle. Besides a directed cycle, this includes a non-clique cycle with directed path $x \to y \to\cdots\to z$ and the edge $xz$ still unoriented: either direction of $xz$ creates a directed cycle or a shortcut.

For example, consider the six-vertex wheel $W_5$ with hub 1 and rim 2-3-4-5-6-2. By Theorem 2, we may assume that vertex 1 is a source, so $1 \to i$ for $2 \le i \le6$. The following is a two-line proof:

1. B$2 \to3$ (Copy 2) O$2 \to6$ (C1-3-2-6) O$5 \to6$ (C1-2-6-5) O$5 \to4$ (C1-4-5-6) O$3 \to4$ (C1-3-4-5) S:1-2-3-4

2. MC$2 \; 3 \to2$ O$6 \to2$ (C1-3-2-6) O$6 \to5$ (C1-2-6-5) O$4 \to5$ (C1-4-5-6) O$4 \to3$ (C1-3-4-5) S:1-4-3-2.

The first line assumes $2 \to3$ and saves the alternative $3 \to2$ as Copy 2. Each O instruction follows from Lemma 1 on the indicated four-cycle. The line ends with $1 \to2 \to3 \to4$ and $1 \to4$, a shortcut because 24 is not an edge. The second line returns to Copy 2 and closes the other branch with the shortcut $1 \to4 \to3 \to2$, again using the missing edge 24. Thus both orientations of 23 are excluded.

To print a proof for a single adjacency-matrix file graph.txt, run the software [17] with

python3 proof_lines.py --txt graph.txt --algorithm 6.

The --zip option reports proof-length statistics for a collection of graphs instead.

Algorithm 1 in [11]

Algorithm 1 sorts the edges according to the number of cycles they belong to and then branches on an edge that belongs to the largest number of cycles (whenever branching is required). If there are two or more such edges, the branching choice is made lexicographically.

Algorithm 2 (Best-Performing in [11]

Algorithm 2 selects a cycle $C$ with the smallest number of unoriented edges. The unoriented edges in $C$ are then sorted, as in Algorithm 1, according to the number of cycles they belong to, and branching is performed on an edge that belongs to the largest number of cycles. If there are two or more such edges, the branching choice is made lexicographically.

Algorithm 3 in [11]

Algorithm 3 is similar to Algorithm 2, but it selects a cycle that has the largest number $N$ of edges oriented in the same direction. Among the cycles with the same value of $N$, Algorithm 3 selects a cycle $C$ with the smallest number of unoriented edges. Then, as in Algorithm 2, the unoriented edges in $C$ are sorted according to the number of cycles they belong to, and branching is performed on an edge that belongs to the largest number of cycles. If there are two or more such edges, the branching choice is made lexicographically.

Algorithm 4 (New)

Algorithm 4 attempts to improve the previously best-performing Algorithm 2 by keeping track of the length of the longest directed path in the current partially oriented graph (the idea being that longer directed paths may lead to more frequent applications of Lemma 1).

Algorithm 4 selects a cycle $C$ with the smallest number of unoriented edges. Among the cycles with the same minimum number of unoriented edges, the choice is made lexicographically. If $C$ contains exactly one unoriented edge, branching is performed on this edge.

Otherwise, for each unoriented edge $e \in C$, Algorithm 4 temporarily orients $e$ in both possible directions and evaluates the resulting increase in the length of the longest directed path in the current partial orientation. For each edge, the maximum increase over the two possible orientations is recorded. The algorithm then selects an edge that maximizes this increase.

If several edges yield the same maximum increase, they are sorted in decreasing order according to the number of cycles they belong to, and branching is performed on the lexicographically smallest among them. If no edge produces a positive increase, Algorithm 4 falls back to the selection rule of Algorithm 3.

Algorithm 5 (New)

Algorithm 5 is another attempt to improve the previously best-performing Algorithm 2. Algorithm 5 selects a cycle $C$ with the smallest number of unoriented edges. Among the cycles with the same minimum number of unoriented edges, the choice is made lexicographically. The unoriented edges in $C$ are then sorted according to the following criteria:

1. decreasing number of cycles the edge belongs to;

2. decreasing sum of the degrees of its endpoints;

3. lexicographic order.

Branching is performed on the first edge in this ordering.

Algorithm 6 (New, Best-Performing)

Algorithm 6 selects the branching edge using a deterministic one-step lookahead procedure. Unlike the previous algorithms, which rely only on local cycle information, Algorithm 6 explicitly simulates the immediate consequences of each candidate branching decision before selecting an edge.

The procedure consists of the following stages.

1. Selection of critical cycles. Among all non-clique cycles (as defined by Lemma 1), we consider only those cycles that contain at least one unoriented edge. For each such cycle, we compute the number of its unoriented edges in the current partial orientation.

We then restrict our attention to the cycles with the minimum number of unoriented edges. These cycles are the most constrained and are closest to being fully oriented. All further branching decisions are derived only from this subset of cycles.

2. Construction of candidate edges. From the selected cycles, we collect all unoriented edges and remove duplicates. These edges form the candidate branching set. If this set contains only one edge, that edge is selected immediately.

3. One-step simulation. For each candidate edge $e = uv$ with $u < v$, both possible orientations are examined:

• Orient $u \to v$;

• Orient $v \to u$.

For each orientation:

1. The current state is copied and the copy is updated by orienting $e$ in the chosen direction.

2. All forced propagation rules are applied: Lemma 1, triangle rule, contradiction detection (directed cycles, shortcuts, or a non-clique cycle whose final unoriented edge would create one of these).

If a contradiction is detected during propagation, the branch is considered immediately closed. Otherwise, we measure the remaining unresolved structure by counting the total number of unoriented cycle-edge incidences in the resulting state, with each edge counted once for each non-clique cycle containing it.

For each candidate edge, we therefore obtain:

• The number of non-contradictory orientations,

• The worst remaining unresolved count among its valid orientations.

• The total remaining unresolved count over its valid orientations.

4. Edge comparison and selection. Candidate edges are compared using a fixed priority order:

1. Prefer edges with fewer non-contradictory orientations (i.e., edges that close more branches immediately).

2. Among those, prefer edges with smaller worst-case remaining unresolved structure.

3. If still tied, prefer edges with smaller total remaining unresolved structure.

4. If still tied, prefer edges that appear in more cycles.

5. If still tied, prefer edges whose endpoints have larger degree sum.

6. Finally, choose the lexicographically smallest edge, using the canonical pairs defined at the start of this section.

The edge that is best under this ordered comparison is selected for branching.

Interpretation. Algorithm 6 can be understood as a deterministic greedy lookahead rule. Instead of choosing an edge based solely on static structural properties, it evaluates the immediate impact of each branching decision and selects the edge with the best score in the stated priority order.

For the pseudocode, let $U_T(C)$ be the number of unoriented edges of cycle $C$ in state $T$, and let

Thus $R(T)$ counts unoriented cycle-edge incidences, rather than distinct edges. The algorithm performs only one level of simulation and therefore remains computationally manageable while incorporating global structural information. Since this algorithm turns out to be the best-performing on average among all six algorithms, as shown by the experimental results in § 2.8, we present its pseudocode in Algorithm 6.

The following observation gives a formal guarantee for the lookahead rule.

Algorithm 6 One-step lookahead branching

Require: $S$ ▷ Current partial orientation state Require: $C$ ▷ Set of non-clique cycles Require: $\operatorname{count}(e)$ ▷ Number of cycles containing each edge Ensure: $e^{*}$ ▷ Selected branching edge, or None

1. $\textit{critical\_cycles} \leftarrow\{C \in\mathcal{C} \mid U_{S}(C) > 0\}$

2. if $\textit{critical\_cycles} = \varnothing$ then

3. &nbsp;&nbsp;&nbsp;&nbsp;return None

4. end if

5. $t \leftarrow\min\{U_{S}(C) \mid C \in\textit{critical\_cycles}\}$

6. $C^{*} \leftarrow\{C \in\textit{critical\_cycles} \mid U_{S}(C) = t\}$

7. $\textit{candidates} \leftarrow$ set of all unoriented edges in cycles in $C^{*}$

8. if $\lvert\textit{candidates}\rvert= 1$ then

9. &nbsp;&nbsp;&nbsp;&nbsp;return the unique edge in $\textit{candidates}$ as $e^{*}$

10. end if

11. for each edge $e = uv$ in $\textit{candidates}$, with $u < v$ do

12. &nbsp;&nbsp;&nbsp;&nbsp;$\textit{unresolved} \leftarrow0$

13. &nbsp;&nbsp;&nbsp;&nbsp;$\textit{worst\_residual} \leftarrow0$

14. &nbsp;&nbsp;&nbsp;&nbsp;$\textit{residual\_sum} \leftarrow0$

15. &nbsp;&nbsp;&nbsp;&nbsp;for each direction $d \in\{u \to v, v \to u\}$ do

16. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$S_{\textit{copy}} \leftarrow\operatorname{clone}(S)$

17. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Update $S_{\textit{copy}}$ by orienting $e$ according to $d$

18. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Apply all forced propagation rules to $S_{\textit{copy}}$

19. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if a contradiction occurs then

20. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;continue with the next direction in the inner loop

21. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;end if

22. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\textit{unresolved} \leftarrow\textit{unresolved} + 1$

23. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$r \leftarrow R(S_{\textit{copy}})$

24. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\textit{residual\_sum} \leftarrow\textit{residual\_sum} + r$

25. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\textit{worst\_residual} \leftarrow\max(\textit{worst\_residual}, r)$

26. &nbsp;&nbsp;&nbsp;&nbsp;end for

27. &nbsp;&nbsp;&nbsp;&nbsp;Assign $e$ the lexicographic score: &nbsp;&nbsp;&nbsp;&nbsp;$(\textit{unresolved}, \textit{worst\_residual}, \textit{residual\_sum}, -\operatorname{count}(e), -\deg(u) - \deg(v), e)$.

28. end for

29. $e^{*} \leftarrow$ edge with minimal lexicographic score

30. return $e^{*}$

Proof. The $2-a$ immediately closed orientations each contribute one terminal branch. In a surviving trial state, the number of distinct unoriented edges belonging to non-clique cycles is at most $r$. Each subsequent branching step orients one of these edges, so the resulting binary subtree has depth at most $r$ and at most $2^r$ terminal branches. This proves the bound. The minimization claim follows from the first three entries of the score. Finally, branching considers both directions, forced orientations are necessary in any semi-transitive extension, and branches are closed only by a directed cycle, a shortcut, or a non-clique cycle whose final unoriented edge would create one of these.

This is a local guarantee; the residual count does not determine the eventual proof length. In particular, it does not establish that Algorithm 6 always gives shorter proofs than the other algorithms. The comparisons below are empirical.

Ranking of algorithms

As noted in [11], making general statements about the efficiency of the algorithms, either in terms of the number of lines they produce or their time complexity, does not seem feasible. However, some indication of the algorithms’ efficiency can be obtained by examining their performance on small non-word-representable graphs. Unfortunately, the first three algorithms were tested in [11] only on non-word-representable graphs with up to seven vertices, which is a very small set. It was observed that Algorithms 2 and 3 have similar performance, with Algorithm 2 being slightly better (and hence used in the software [14]), while Algorithm 1 was much worse.

In Table 1 we confirm the ranking of Algorithms 1–3 on graphs with up to nine vertices and extend the comparison by including Algorithms 4–6. On average, a clear winner is Algorithm 6, with Algorithms 2–5 performing similarly and Algorithm 1 being much worse (on nine vertices, the performance difference between the best and worst algorithms is a factor of about 2.09, and between the best and the next-best algorithms a factor of about 1.31).

	Alg. 1	Alg. 2	Alg. 3	Alg. 4	Alg. 5	Alg. 6
6 vertices	10	8	8	8	8	8
7 vertices	12.880	8.080	8.280	8.000	8.080	8.880
8 vertices	16.637	12.139	12.374	12.252	12.135	9.688
9 vertices	22.350	14.046	14.218	14.256	14.045	10.703

Interestingly, in the worst-case scenario (when the longest proofs are produced), Algorithm 6 significantly outperforms all other algorithms (on nine vertices, the performance difference ratio is between about 2.18 and 2.68), while Algorithm 1 is not the worst in the worst-case scenario on eight and nine vertices. We refer to Table 2 for the recorded observations and to Figure 5, where the graphs requiring long proofs are presented (their names come from the database [16]).

	Worst 7	graphs	Worst 8	graphs	Worst 9	graphs
Alg. 1	28	1	56	32, 39, 367, 493	200	5338
Alg. 2	12	1, 6	60	845	228	54062
Alg. 3	14	19	52	845	185	6392
Alg. 4	12	1	52	845	188	46392
Alg. 5	12	1, 6	60	845	228	54062
Alg. 6	12	1	23	149, 818	85	5813

Algorithm 6 was implemented in software [17].

Applications of Algorithm 6

The Shrikhande graph and the Clebsch graph were used in [11] as a proof of concept for automatically generating proofs of non-word-representability for rather large graphs, for which finding proofs would otherwise be considered a challenging problem. A 10-line proof of non-word-representability of a certain minimal non-word-representable subgraph $C$ of the Clebsch graph using Algorithm 2 was produced in [11]. Algorithm 6 also produces a 10-line proof (both on $C$ and on the entire Clebsch graph); hence, we omit the discussion of the Clebsch graph here.

However, Algorithm 6 does shorten the 6-line proof given in [11] of non-word-representability of the minimal non-word-representable subgraph $S$ of the Shrikhande graph. Both of these graphs are presented in Figure 2. By applying the same assumption on $S$ that vertex 1 is a source (as done in [11]), Algorithm 6 produces the following 4-line proof.

1. B2→3 (Copy 2) O4→3 (C1-2-3-4) O4→5 (C1-3-4-5) O6→5 (C1-4-5-6) B6→9 (Copy 3) O5→9 (C1-5-9-6) O8→9 O4→8 (C4-5-9-8) O3→8 (C1-3-8-4) O7→9 O2→7 (C2-3-8-9-7) O7→5 (C5-6-9-7) S:1-2-7-5

2. MC3 9→6 O9→7 O7→5 (C5-6-9-7) O9→5 (C1-5-9-6) O7→2 (C1-2-7-5) O8→3 O9→8 (C2-3-8-9-7) O4→8 (C4-5-9-8) S:1-4-8-3

3. MC2 3→2 O3→4 (C1-2-3-4) O5→4 (C1-3-4-5) O5→6 (C1-4-5-6) B6→9 (Copy 4) O7→9 O5→7 (C5-6-9-7) O5→9 (C1-5-9-6) O2→7 (C1-2-7-5) O3→8 O8→9 (C2-3-8-9-7) O8→4 (C4-5-9-8) S:1-3-8-4

4. MC4 9→6 O9→5 (C1-5-9-6) O9→8 O8→4 (C4-5-9-8) O8→3 (C1-3-8-4) O9→7 O7→2 (C2-3-8-9-7) O5→7 (C5-6-9-7) S:1-5-7-2.

As for the subgraph $S$ of the Kneser graph $K(8, 3)$ in Figure 3, for which no published proof of non-word-representability exists so far, one can use the software [14] and assume that vertex 1 is a source to produce (in 25 seconds) a 136-line proof. However, with the same assumption, Algorithm 6 gives a much shorter proof of 110 lines, which we do not include in this paper because of its size (it would take about four pages); instead, we post the proof online at [17].

Concluding remarks

In this paper, we introduced an algorithm that significantly outperforms the best algorithm presented in [11] for automatically generating proofs of non-word-representability of graphs that can be verified by a human. The algorithm was implemented in publicly available software [17], which substantially enlarges the set of graphs for which robust, human-verifiable proofs of non-word-representability can be produced. This advancement is expected to have a notable impact on future developments in the theory of word-representable graphs.

We leave it as an open problem to further improve Algorithm 6. A natural starting point for generating ideas is to analyze the graphs in Figure 5 that require long proofs (for Algorithm 6, these are Graphs 1, 149, 818, and 5813) and to investigate whether different choices of branching vertices can reduce proof length. For example, for Graph 5813, is it possible to produce a proof shorter than 85 lines? This question is interesting in itself: constructing a shorter, ad-hoc proof for Graph 5813 could indicate that Algorithm 6 can indeed be improved.

We conclude by reiterating the following points from [11]: estimating the average efficiency of our algorithms, or of future algorithms, based on certain graph parameters (such as the number of cycles) is a challenging theoretical problem. Likewise, the time complexity of our algorithms presents an intriguing and challenging direction for research, which we have not addressed here because, as in [11], our focus was on producing short proofs.