Encontrar caminos en una subdivisión de $K_5$

Question

Hace algunos años (durante mi tesis de maestría), estudié un problema conocido como La conjetura de Kotzig (pero no este famoso pero el menos conocido en $k$ -trayectos en los gráficos).

De todos modos, no había manera de resolver el problema, pero pude destilar una instancia específica de un subproblema, que parecía bastante fácil. Sin embargo, no fui capaz de resolverlo. Aquí está.

Pregunta.

Toma el $K_5$ (gráfico completo en $5$ vértices), y subdividir sus aristas insertando nuevos vértices (ver la imagen inferior). Sólo hay una condición: como puedes ver, he utilizado sugestivamente diferentes colores para las aristas para dividir el gráfico en un "ciclo exterior" y un "ciclo interior". La condición ahora es, que ambos ciclos deben tener el mismo número de vértices en él, es decir, ambos ciclos deben tener la misma longitud, digamos $k+1$ .

¿Existen siempre dos caminos (no necesariamente libres de intersección) $P_1$ y $P_2$ de longitud $k$ que comienzan en el mismo vértice y terminan en el mismo vértice?

Hice la experiencia, que dado cualquier caso específico del problema, no tenía ningún problema para encontrar tal doble- $k$ -senda. Pero me resultó muy difícil (incluso imposible), dar una construcción general de tal. Tenía muchas heurísticas, pero las condiciones para su aplicación eran complicadas.

La siguiente imagen muestra dos caminos de 12 en la subdivisión anterior con 13 ciclos.

Answer 1

Etiquetar los vértices del original $K_5$ como $u_i\;(i \in [1,5])$ . Sea $w_{i,j}\;(i,j \in [1,5])$ sea uno mayor que el número de vértices insertados en la arista $u_i - u_j$ . Entonces podemos etiquetar esos vértices intermedios $v_{i,j,a}$ numerado $u_i - v_{i,j,1} - v_{i,j,2} - \cdots - v_{i,j,w_{i,j}-1} - u_j$ con identificación $v_{i,j,a} = v_{j,i,w_{i,j}-a}$ .

La restricción de generación es que $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$ .

Dejemos que $G_5$ denotan el original $K_5$ con pesos $w_{i,j}$ y $G_5 \setminus (u_i, u_j)$ denota el gráfico obtenido al eliminar la arista $(u_i, u_j)$ de $G_5$ .

Denota los puntos finales compartidos de $P_1$ y $P_2$ como $s$ y $t$ .

Hay cinco casos:

• $s = u_i, t = u_j$ son ambos vértices de $G_5$ . Entonces los dos caminos $s -^* t$ en el gráfico subdividido tienen los mismos pesos que los caminos en $G_5$ que pasan por los mismos vértices en el mismo orden. Dado que $w_{i,j} \le k - 3$ podemos ignorar el borde directo $u_i - u_j$ Así que buscamos dos caminos $u_i -^* u_j$ en $G_5 \setminus (u_i, u_j)$ de peso $k$ .
• $s = u_i$ es un vértice de $G_5$ y $t = v_{i,j,a}$ es un vértice intermedio en una arista desde $s$ . Como de nuevo una aproximación directa es demasiado corta, buscamos dos caminos $u_i -^* u_j$ en $G_5 \setminus (u_i, u_j)$ de peso $k - (w_{i,j} - a)$ .
• $s = v_{i,j,a}, t = v_{i,j,b}, a < b$ son vértices intermedios en la misma arista. Podemos aumentar o disminuir $a$ y $b$ juntos, así que esto no añade nada al caso anterior.
• $s = u_i$ es un vértice de $G_5$ y $t = v_{h,j,a}$ es un vértice intermedio en una arista independiente de $s$ . Entonces podemos tener dos caminos a través de $u_h$ (es decir, caminos $u_i -^* u_h$ en $G_5 \setminus (u_h,u_j)$ de peso $k - a$ ), dos caminos a través de $u_j$ (es decir, caminos $u_i -^* u_j$ en $G_5 \setminus(u_h, u_j)$ de peso $k - (w_{h,j} - a)$ ), o uno de cada uno.
• $s = v_{i,j,a}, t = v_{m,n,b}$ son vértices intermedios en aristas diferentes. Luego hay cuatro opciones, que siguen los patrones anteriores.

En conjunto, obtenemos una gigantesca pero finita disyunción de conjunciones de desigualdades que podemos negar y alimentar a un solucionador de satisfacciones como Z3.

---

Para generar la fuente Z3 estoy usando Python. Probablemente volveré a esto y trataré de ordenarlo un poco. Resultó no ser necesario para cubrir completamente el caso final. Me doy cuenta de que las pruebas informáticas no son tan satisfactorias como las no informáticas, pero al menos saber que es un teorema es un buen punto de partida.

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)")