Finding paths in a subdivision of $K_5$

Question

Some years ago (during my master's thesis), I studied a problem known as Kotzig's conjecture (however not this famous one, but the lesser known one on $k$-paths in graphs).

Anyway, there was no way to solve the problem, but I was able to distill one specific instance of a sub-problem, that seemed easy enough. Still, I was not able to solve it. Here it is.

Question.

Take the $K_5$ (complete graph on $5$ vertices), and subdivide its edges by inserting new vertices (see the image below). There is only one condition: as you can see, I suggestively used different colors for the edges to divide the graph into an "outer cycle" and an "inner cycle". The condition now is, that both cycles must have the same number of vertices in it, i.e., both cycles must have the same length, say $k+1$.

Do there always exists two (not necessarily intersection-free) paths $P_1$ and $P_2$ of length $k$, that start in the same vertex, and end in the same vertex?

I made the experience, that given any specific instance of the problem, I had no trouble finding such a double-$k$-path. But I found it very hard (even impossible), to give a general construction of such one. I had a lot of heuristics, but the conditions for their applications where complicated.

The following image shows two 12-paths in the above subdivision with 13-cycles.

Answer 1

Label the vertices of the original $K_5$ as $u_i\;(i \in [1,5])$. Let $w_{i,j}\;(i,j \in [1,5])$ be one greater than the number of vertices inserted in the edge $u_i - u_j$. Then we can label those intermediate vertices $v_{i,j,a}$ numbered $u_i - v_{i,j,1} - v_{i,j,2} - \cdots - v_{i,j,w_{i,j}-1} - u_j$ with identification $v_{i,j,a} = v_{j,i,w_{i,j}-a}$.

The generation constraint is that $w_{1,2} + w_{2,3} + w_{3,4} + w_{4,5} + w_{1,5} = w_{1,3} + w_{3,5} + w_{2,5} + w_{2,4} + w_{1,4} = k + 1$.

Let $G_5$ denote the original $K_5$ with weights $w_{i,j}$, and $G_5 \setminus (u_i, u_j)$ denote the graph obtained by deleting edge $(u_i, u_j)$ from $G_5$.

Denote the shared endpoints of $P_1$ and $P_2$ as $s$ and $t$.

There are five cases:

• $s = u_i, t = u_j$ are both vertices of $G_5$. Then the two paths $s -^* t$ in the subdivided graph have the same weights as the paths in $G_5$ which pass through the same vertices in the same order. Since $w_{i,j} \le k - 3$ we can ignore the direct edge $u_i - u_j$, so we're looking for two paths $u_i -^* u_j$ in $G_5 \setminus (u_i, u_j)$ of weight $k$.
• $s = u_i$ is a vertex of $G_5$, and $t = v_{i,j,a}$ is an intermediate vertex on an edge from $s$. Since again a direct approach is too short, we're looking for two paths $u_i -^* u_j$ in $G_5 \setminus (u_i, u_j)$ of weight $k - (w_{i,j} - a)$.
• $s = v_{i,j,a}, t = v_{i,j,b}, a < b$ are intermediate vertices on the same edge. We can increment or decrement $a$ and $b$ together, so this doesn't add anything to the previous case.
• $s = u_i$ is a vertex of $G_5$, and $t = v_{h,j,a}$ is an intermediate vertex on an edge independent of $s$. Then we can have two paths through $u_h$ (i.e. paths $u_i -^* u_h$ in $G_5 \setminus (u_h,u_j)$ of weight $k - a$), two paths through $u_j$ (i.e. paths $u_i -^* u_j$ in $G_5 \setminus(u_h, u_j)$ of weight $k - (w_{h,j} - a)$), or one of each.
• $s = v_{i,j,a}, t = v_{m,n,b}$ are intermediate vertices on different edges. Then there are four options, which follow the previous patterns.

Put together, we get a giant but finite disjunction of conjunctions of inequalities which we can negate and feed to a satisfiability solver such as Z3.

---

To generate the Z3 source I'm using Python. I'll probably come back to this and try to tidy it up a bit. It turned out not to be necessary to fully cover the final case. I realise that computer proofs aren't as satisfactory as non-computer proofs, but at least knowing that it's a theorem is a good starting point.

from itertools import permutations, combinations

for i, j in combinations(range(1, 6), 2):
    print("(declare-const w{}{} Int)".format(i, j))
print("(declare-const k Int)")

for i, j in combinations(range(1, 6), 2):
    print("(assert (> w{}{} 0))".format(i, j))
print("(assert (= (+ w12 w23 w34 w45 w15) (+ w13 w35 w25 w24 w14) (+ k 1)))")

# Assert the non-existence of two paths of length k between the same vertices
print("(assert (not(or")


def path_weight(path):
    rv = "(+"
    u = path[0]
    for v in path[1:]:
        rv += " w{}{}".format(min(u, v), max(u, v))
        u = v
    rv += ")"
    return rv

def paths(s, t, excluded_edges):
    s, t = min(s, t), max(s, t)
    excluded_edges = ["w{}{}".format(min(i, j), max(i, j)) for i, j in excluded_edges]

    paths_st = set()
    other_vertices = set(range(1, 6))
    other_vertices.remove(s)
    other_vertices.remove(t)
    for pathlen in range(0, 4):
        for intermediates in permutations(other_vertices, pathlen):
            path = tuple([s] + list(intermediates) + [t])
            path_str = path_weight(path)
            if not any(excluded_edge in path_str for excluded_edge in excluded_edges):
                paths_st.add(path)
    return paths_st

def w(i, j):
    return "w{}{}".format(min(i, j), max(i, j))


for i, j in combinations(range(1, 6), 2):
    # Case 1: two paths from i to j of length k
    # Cases 2 and 3: two paths from i to j of length (k + 1 - w{i}{j}) <= x < k
    # Combined cases 1 to 3: two paths from i to j of length (k + 1 - w{i}{j}) <= x <= k
    paths_ij = paths(i, j, [(i, j)])
    for p1, p2 in combinations(paths_ij, 2):
        path_weight_1 = path_weight(p1)
        path_weight_2 = path_weight(p2)
        #print("\t(and (= path_weight_1 path_weight_2) (<= (+ k 1) (+ path_weight_1 wij)) (<= path_weight_1 k))")
        print("\t(and (= {} {}) (<= (+ k 1) (+ {} {})) (<= {} k))".format(path_weight_1, path_weight_2, path_weight_1, w(i,j), path_weight_1))

for h, j in combinations(range(1, 6), 2):
    avail = set(range(1, 6))
    avail.remove(h)
    avail.remove(j)
    for i in avail:
        # Case 4: two kinds of path: h-*i of weight k-a or h-*j of weight k+a-w_{h,j}, disallowing edge h-j.
        paths_ih = paths(i, h, [(h, j)])
        paths_ij = paths(i, j, [(h, j)])

        for p1, p2 in combinations(paths_ih, 2):
            path_weight_1 = path_weight(p1)
            path_weight_2 = path_weight(p2)
            print("\t(and (= {} {}) (<= (+ k 1) (+ {} {})) (<= (+ {} 1) k))".format(path_weight_1, path_weight_2, path_weight_1, w(h,j), path_weight_1))

        for p1, p2 in combinations(paths_ij, 2):
            path_weight_1 = path_weight(p1)
            path_weight_2 = path_weight(p2)
            print("\t(and (= {} {}) (<= (+ k 1) (+ {} {})) (<= (+ {} 1) k))".format(path_weight_1, path_weight_2, path_weight_1, w(h,j), path_weight_1))

        for p1 in paths_ih:
            path_weight_1 = path_weight(p1)
            for p2 in paths_ij:
                path_weight_2 = path_weight(p2)
                # path_weight_1 = (k - a) and path_weight_2 = k - (w_{h,j} - a) and 0 < a < w_{h,j}
                # Rearrange: 0 < a = k - path_weight_1 = path_weight_2 - k + w_{h,j} < w_{h,j}
                #   2k = path_weight_1 + path_weight_2 + w_{h,j}
                #   path_weight_1 < k
                #   path_weight_2 < k
                print("\t(and (= (+ k k) (+ {} {} {})) (< {} k) (< {} k))".format(path_weight_1, path_weight_2, w(h,j), path_weight_1, path_weight_2))

# How to keep this from getting too messy?
# s = v_{i,j,a}  t = v_{m,n,b}
# Two paths in G_5 \ {(u_i, u_j), (u_m, u_n)}
# * Two paths through u_i -* u_m            so i != m
for i in range(1, 6):
    for j in (x for x in range(1, 6) if x != i):
        for m in (x for x in range(1, 6) if x != i):
            for n in (x for x in range(1, 6) if x != m):
                if sorted([i, j]) == sorted([m, n]): continue
                paths_im = paths(i, m, [(i, j), (m, n)])
                for p1, p2 in combinations(paths_im, 2):
                    path_weight_1 = path_weight(p1)
                    path_weight_2 = path_weight(p2)
                    # Two paths i-*m of same weight, between k-(w_{i,j}-1)-(w_{m,n}-1) and k-2
                    print("\t(and (= {} {}) (<= (+ k 2) (+ {} {} {})) (<= (+ {} 2) k))".format(path_weight_1, path_weight_2, path_weight_1, w(i,j), w(m,n), path_weight_1))

# * One path through u_i -* u_m and one through u_i -* u_n          i != m, i != n
for i in range(1, 6):
    for j in (x for x in range(1, 6) if x != i):
        for m, n in combinations((x for x in range(1, 6) if x != i), 2):
            paths_im = paths(i, m, [(i, j), (m, n)])
            paths_in = paths(i, n, [(i, j), (m, n)])
            for p1 in paths_im:
                path_weight_1 = path_weight(p1)
                for p2 in paths_in:
                    path_weight_2 = path_weight(p2)
                    # s = v_{i,j,a}  t = v_{m,n,b}
                    # 
                    # a + path_weight_1 + b = a + path_weight_2 + w_{m,n} - b = k
                    # 1 <= a <= w_{i,j} - 1
                    # 1 <= b <= w_{m,n} - 1
                    #
                    # 2b = path_weight_2 + w_{m,n} - path_weight_1
                    # 2a = 2k - (path_weight_1 + path_weight_2 + w_{m,n})
                    #
                    # (= 0 (% (+ path_weight_1 path_weight_2 w_{m,n}) 2))
                    # (<= (+ 2 path_weight_1 path_weight_2 w_{m,n}) (+ k k))
                    # (<= (+ k k 2) (+ w_{i,j} w_{i,j} path_weight_1 path_weight_2 w_{m,n}))
                    # (<= (+ 2 path_weight_1) (+ path_weight_2 w_{m,n}))
                    # (<= (+ 2 path_weight_2 w_{m,n}) (+ path_weight_1 w_{m,n} w_{m,n}))
                    print(("\t(and (= 0 (mod (+ {} {} {}) 2)) " +
                           "(<= (+ 2 {} {} {}) (+ k k)) " +
                           "(<= (+ k k 2) (+ {} {} {} {} {})) " +
                           "(<= (+ 2 {}) (+ {} {})) " +
                           "(<= (+ 2 {} {}) (+ {} {} {})))").format(
                               path_weight_1, path_weight_2, w(m,n),
                               path_weight_1, path_weight_2, w(m,n),
                               w(i,j), w(i,j), path_weight_1, path_weight_2, w(m,n),
                               path_weight_1, path_weight_2, w(m,n),
                               path_weight_2, w(m,n), path_weight_1, w(m,n), w(m,n)))


# * One path through u_i -* u_m and one through u_j -* u_n
# Turns out not to be necessary.

print(")))")

print("(check-sat)")