Claude Code transcript - page 2/4

#!/usr/bin/env python3
"""
Search for counterexamples to BSC (k-1)-resilient forwarding for k=6.

We search for:
1. Loops in the bounce-circular strategy with various arborescence constructions
2. Small graphs where NO BSC strategy achieves 5-resiliency

A BSC forwarding function at vertex v maps (incoming_arb, failed_arbs_at_v) -> chosen_arb.
This is equivalent to a priority ordering of arborescences for each (vertex, incoming_arb).
"""

import networkx as nx
import itertools
import random
import sys
from collections import defaultdict


def find_arborescences_randomized(G, root, k, seed=0):
    """Find k arc-disjoint arborescences via randomized greedy BFS.
    Returns list of dicts: arb[v] = parent of v (toward root), or None for root.
    Returns None on failure."""
    rng = random.Random(seed)
    nodes = sorted(G.nodes())
    n = len(nodes)

    # Available arcs (as a set of (u,v) directed edges)
    avail = set()
    for u, v in G.edges():
        avail.add((u, v))
        avail.add((v, u))

    arborescences = []
    for t in range(k):
        parent = {root: None}
        queue = [root]
        while queue:
            u = queue.pop(0)
            # Randomize neighbor order for diversity
            neighbors = [v for v in nodes if v not in parent and (v, u) in avail]
            rng.shuffle(neighbors)
            for v in neighbors:
                if v not in parent:
                    parent[v] = u
                    queue.append(v)
        if len(parent) < n:
            return None
        arborescences.append(parent)
        # Remove used arcs
        for v, p in parent.items():
            if p is not None:
                avail.discard((v, p))
    return arborescences


class BSCSimulator:
    """Simulates BSC forwarding on a graph with arc-disjoint arborescences."""

    def __init__(self, G, root, arborescences):
        self.G = G
        self.root = root
        self.arbs = arborescences
        self.k = len(arborescences)
        self.n = G.number_of_nodes()

        # out_arc[(v, i)] = w means arborescence i sends v to w
        self.out_arc = {}
        for i, arb in enumerate(self.arbs):
            for v, p in arb.items():
                if p is not None:
                    self.out_arc[(v, i)] = p

        # arc_to_arb[(v, w)] = i means arc (v,w) belongs to arborescence i
        self.arc_to_arb = {}
        for i, arb in enumerate(self.arbs):
            for v, p in arb.items():
                if p is not None:
                    self.arc_to_arb[(v, p)] = i

    def failed_arbs_at(self, v, failure_set):
        """Return set of arborescence indices with failed outgoing arcs at v."""
        failed = set()
        for i in range(self.k):
            if (v, i) in self.out_arc:
                w = self.out_arc[(v, i)]
                if frozenset({v, w}) in failure_set:
                    failed.add(i)
        return failed

    def bounce_target(self, v, arb_i):
        """Return bounce arborescence index when arb_i fails at v, or None."""
        if (v, arb_i) not in self.out_arc:
            return None
        w = self.out_arc[(v, arb_i)]
        if (w, v) in self.arc_to_arb:
            j = self.arc_to_arb[(w, v)]
            if j != arb_i:
                return j
        return None

    def simulate(self, source, failure_set, strategy):
        """
        Simulate BSC forwarding.

        strategy: callable(vertex, current_arb, failed_set_at_v, simulator) -> next_arb
            Must return an arborescence index not in failed_set_at_v.

        Returns (delivered: bool, looped: bool)
        """
        v = source
        arb = strategy(v, None, self.failed_arbs_at(v, failure_set), self)
        if arb is None:
            return False, False

        visited = set()
        max_steps = self.k * self.n * 4

        for _ in range(max_steps):
            if v == self.root:
                return True, False

            state = (v, arb)
            if state in visited:
                return False, True
            visited.add(state)

            # Check current arb
            if (v, arb) not in self.out_arc:
                return False, False
            w = self.out_arc[(v, arb)]

            if frozenset({v, w}) not in failure_set:
                # Canonical forward
                v = w
                continue

            # Failed. Use strategy to pick next arb.
            failed_here = self.failed_arbs_at(v, failure_set)
            next_arb = strategy(v, arb, failed_here, self)
            if next_arb is None or next_arb in failed_here:
                return False, False  # Dead end

            arb = next_arb
            w2 = self.out_arc[(v, arb)]
            v = w2

        return False, True  # Exceeded steps


def bounce_circular_strategy(circular_order):
    """Create a bounce-first, circular-fallback BSC strategy."""
    k = len(circular_order)

    def strategy(v, current_arb, failed_set, sim):
        if current_arb is None:
            # Initial: pick first non-failed in circular order
            for a in circular_order:
                if a not in failed_set:
                    return a
            return None

        # Try bounce first
        bt = sim.bounce_target(v, current_arb)
        if bt is not None and bt not in failed_set:
            return bt

        # Circular fallback
        try:
            pos = circular_order.index(current_arb)
        except ValueError:
            pos = 0
        for offset in range(1, k):
            a = circular_order[(pos + offset) % k]
            if a not in failed_set:
                return a
        return None

    return strategy


def circular_only_strategy(circular_order):
    """Pure circular strategy (no bouncing)."""
    k = len(circular_order)

    def strategy(v, current_arb, failed_set, sim):
        if current_arb is None:
            for a in circular_order:
                if a not in failed_set:
                    return a
            return None
        try:
            pos = circular_order.index(current_arb)
        except ValueError:
            pos = 0
        for offset in range(1, k):
            a = circular_order[(pos + offset) % k]
            if a not in failed_set:
                return a
        return None

    return strategy


def min_depth_strategy():
    """Switch to arborescence with minimum depth at current vertex."""
    def strategy(v, current_arb, failed_set, sim):
        best = None
        best_depth = float('inf')
        for i in range(sim.k):
            if i not in failed_set and (v, i) in sim.out_arc:
                d = 0
                u = v
                while u != sim.root:
                    if (u, i) not in sim.out_arc:
                        d = float('inf')
                        break
                    u = sim.out_arc[(u, i)]
                    d += 1
                    if d > sim.n:
                        d = float('inf')
                        break
                if d < best_depth:
                    best_depth = d
                    best = i
        return best

    return strategy


def test_graph(G, root, k, max_failures, verbose=False):
    """Test all strategies on a graph. Returns info about any loops found."""
    results = []

    # Try multiple arborescence constructions
    for seed in range(20):
        arbs = find_arborescences_randomized(G, root, k, seed=seed)
        if arbs is None:
            continue

        sim = BSCSimulator(G, root, arbs)
        edges = list(G.edges())
        num_edges = len(edges)

        # Build strategies to test
        strategies = {}

        # Various circular orderings
        for name, order in [
            ("interleaved_031425", [0, 3, 1, 4, 2, 5]),
            ("sequential_012345", [0, 1, 2, 3, 4, 5]),
            ("alt_interleave", [0, 2, 4, 1, 3, 5]),
        ]:
            strategies[f"bounce_circ_{name}"] = bounce_circular_strategy(order)
            strategies[f"circ_only_{name}"] = circular_only_strategy(order)

        # Add random orderings
        rng = random.Random(seed * 1000)
        for ri in range(5):
            perm = list(range(k))
            rng.shuffle(perm)
            strategies[f"bounce_circ_rand{ri}"] = bounce_circular_strategy(perm)

        # Min-depth strategy
        strategies["min_depth"] = min_depth_strategy()

        # Test failure sets
        if num_edges <= 20:
            fail_combos = list(itertools.combinations(range(num_edges), max_failures))
        else:
            # Sample
            fail_combos = set()
            rng2 = random.Random(42 + seed)
            for _ in range(min(10000, num_edges ** 2)):
                fc = tuple(sorted(rng2.sample(range(num_edges), max_failures)))
                fail_combos.add(fc)
            # Also try smaller failure sets
            for sz in range(1, max_failures):
                for _ in range(min(2000, num_edges ** 2)):
                    fc = tuple(sorted(rng2.sample(range(num_edges), sz)))
                    fail_combos.add(fc)
            fail_combos = list(fail_combos)

        for fc in fail_combos:
            failure_set = set()
            for idx in fc:
                u, v = edges[idx]
                failure_set.add(frozenset({u, v}))

            # Check graph stays connected
            H = G.copy()
            for fe in failure_set:
                u, v = tuple(fe)
                if H.has_edge(u, v):
                    H.remove_edge(u, v)
            if not nx.is_connected(H):
                continue

            for sname, strat in strategies.items():
                for source in G.nodes():
                    if source == root:
                        continue
                    delivered, looped = sim.simulate(source, failure_set, strat)
                    if not delivered:
                        result = {
                            'graph_edges': list(G.edges()),
                            'n': G.number_of_nodes(),
                            'root': root,
                            'source': source,
                            'seed': seed,
                            'strategy': sname,
                            'failure_set': [tuple(fe) for fe in failure_set],
                            'looped': looped,
                            'arbs': [{v: p for v, p in arb.items() if p is not None}
                                     for arb in arbs],
                        }
                        results.append(result)
                        if verbose:
                            tag = "LOOP" if looped else "DEAD END"
                            print(f"  [{tag}] seed={seed} strat={sname} "
                                  f"src={source} failures={len(fc)} "
                                  f"fail={[edges[i] for i in fc]}")

    return results


def main():
    random.seed(42)
    k = 6
    max_failures = 5  # k - 1

    print(f"Searching for counterexamples to BSC {k-1}-resilient forwarding (k={k})")
    print(f"Looking for graphs where bounce-circular and other BSC strategies fail")
    print()

    trial_count = 0
    total_loops = 0

    for trial in range(200):
        # Generate random 6-connected graphs of various sizes
        n = random.choice([8, 9, 10, 11, 12])

        G = None
        for _ in range(200):
            p = random.uniform(0.45, 0.85)
            G_try = nx.gnp_random_graph(n, p, seed=random.randint(0, 10**7))
            if (G_try.number_of_nodes() == n and
                nx.is_connected(G_try) and
                nx.edge_connectivity(G_try) >= k):
                G = G_try
                break

        if G is None:
            continue

        trial_count += 1
        num_edges = G.number_of_edges()
        print(f"Trial {trial_count}: n={n}, m={num_edges}, "
              f"edge_conn={nx.edge_connectivity(G)}")

        results = test_graph(G, root=0, k=k, max_failures=max_failures,
                             verbose=True)

        if results:
            loop_results = [r for r in results if r['looped']]
            total_loops += len(loop_results)

            # Check if ALL strategies fail for some failure set
            # Group by (failure_set_key, source)
            failure_sources = defaultdict(set)
            for r in results:
                key = (tuple(sorted(tuple(sorted(fe)) for fe in r['failure_set'])),
                       r['source'], r['seed'])
                failure_sources[key].add(r['strategy'])

            # Find cases where many strategies fail
            for key, strats in failure_sources.items():
                if len(strats) >= 5:
                    fail_edges, src, seed = key
                    print(f"  ** {len(strats)} strategies fail: "
                          f"src={src} fail={fail_edges} seed={seed}")
                    print(f"     Failing strategies: {sorted(strats)}")
        else:
            print(f"  No loops found")

        if trial_count >= 50:
            break

    print(f"\nSummary: {trial_count} graphs tested, {total_loops} total loops found")

    if total_loops > 0:
        print("\nCounterexamples to specific strategies were found.")
        print("This shows the bounce-circular strategy does not trivially extend to k=6")
        print("without the Lemma 3 edge-disjoint partition construction.")
    else:
        print("\nNo counterexamples found in this search.")
        print("The conjecture may hold for k=6, but more extensive search is needed.")


if __name__ == '__main__':
    main()

#!/usr/bin/env python3
"""
Search v2: Focus on sparser 6-connected graphs and exhaustive enumeration.
Also check arborescence structure (edge sharing) to understand why no loops found.
"""

import networkx as nx
import itertools
import random
from collections import defaultdict


def find_arborescences(G, root, k, seed=0):
    """Find k arc-disjoint arborescences via randomized greedy."""
    rng = random.Random(seed)
    nodes = sorted(G.nodes())
    n = len(nodes)
    avail = set()
    for u, v in G.edges():
        avail.add((u, v))
        avail.add((v, u))
    arborescences = []
    for _ in range(k):
        parent = {root: None}
        queue = [root]
        while queue:
            u = queue.pop(0)
            nbrs = [v for v in nodes if v not in parent and (v, u) in avail]
            rng.shuffle(nbrs)
            for v in nbrs:
                if v not in parent:
                    parent[v] = u
                    queue.append(v)
        if len(parent) < n:
            return None
        arborescences.append(parent)
        for v, p in parent.items():
            if p is not None:
                avail.discard((v, p))
    return arborescences


def analyze_arborescences(arbs):
    """Analyze edge sharing between arborescences."""
    k = len(arbs)
    # Collect all arcs
    arcs_by_edge = defaultdict(list)  # frozenset({u,v}) -> [(arc, arb_idx)]
    for i, arb in enumerate(arbs):
        for v, p in arb.items():
            if p is not None:
                arcs_by_edge[frozenset({v, p})].append(((v, p), i))
    shared = sum(1 for e, alist in arcs_by_edge.items() if len(alist) >= 2)
    total = len(arcs_by_edge)
    return shared, total


def simulate(nodes, root, arbs, failure_set, source, strategy_fn):
    """Simulate BSC forwarding. Returns (delivered, looped)."""
    k = len(arbs)
    n = len(nodes)

    out_arc = {}
    for i, arb in enumerate(arbs):
        for v, p in arb.items():
            if p is not None:
                out_arc[(v, i)] = p

    arc_to_arb = {}
    for i, arb in enumerate(arbs):
        for v, p in arb.items():
            if p is not None:
                arc_to_arb[(v, p)] = i

    def is_failed(u, v):
        return frozenset({u, v}) in failure_set

    def failed_at(v):
        return {i for i in range(k) if (v, i) in out_arc and is_failed(v, out_arc[(v, i)])}

    def bounce_target(v, arb_i):
        if (v, arb_i) not in out_arc:
            return None
        w = out_arc[(v, arb_i)]
        if (w, v) in arc_to_arb:
            j = arc_to_arb[(w, v)]
            return j if j != arb_i else None
        return None

    v = source
    f = failed_at(v)
    arb = strategy_fn(v, None, f, k, bounce_target, out_arc)
    if arb is None:
        return False, False

    visited = set()
    for _ in range(k * n * 4):
        if v == root:
            return True, False
        state = (v, arb)
        if state in visited:
            return False, True
        visited.add(state)

        if (v, arb) not in out_arc:
            return False, False
        w = out_arc[(v, arb)]

        if not is_failed(v, w):
            v = w
            continue

        f = failed_at(v)
        next_arb = strategy_fn(v, arb, f, k, bounce_target, out_arc)
        if next_arb is None or next_arb in f:
            return False, False
        arb = next_arb
        if (v, arb) not in out_arc:
            return False, False
        v = out_arc[(v, arb)]

    return False, True


def make_bounce_circular(order):
    def strat(v, cur, failed, k, bounce_fn, out_arc):
        if cur is None:
            for a in order:
                if a not in failed:
                    return a
            return None
        bt = bounce_fn(v, cur)
        if bt is not None and bt not in failed:
            return bt
        try:
            pos = order.index(cur)
        except ValueError:
            pos = 0
        for off in range(1, k):
            a = order[(pos + off) % k]
            if a not in failed:
                return a
        return None
    return strat


def make_circular(order):
    def strat(v, cur, failed, k, bounce_fn, out_arc):
        if cur is None:
            for a in order:
                if a not in failed:
                    return a
            return None
        try:
            pos = order.index(cur)
        except ValueError:
            pos = 0
        for off in range(1, k):
            a = order[(pos + off) % k]
            if a not in failed:
                return a
        return None
    return strat


def generate_sparse_6connected(n, rng):
    """Generate a sparser 6-connected graph by starting from K_n and removing edges."""
    G = nx.complete_graph(n)
    edges = list(G.edges())
    rng.shuffle(edges)
    for u, v in edges:
        G.remove_edge(u, v)
        if nx.edge_connectivity(G) < 6:
            G.add_edge(u, v)
    return G


def generate_near_6regular(n, rng):
    """Try to generate a near-6-regular 6-connected graph."""
    if n < 7:
        return None
    # Start with a 6-regular graph via random_regular_graph
    try:
        G = nx.random_regular_graph(6, n, seed=rng.randint(0, 10**7))
        if nx.edge_connectivity(G) >= 6:
            return G
    except:
        pass
    return None


def test_exhaustive(G, root, arbs, k, max_fail):
    """Exhaustively test all failure sets up to max_fail for ALL orderings."""
    nodes = sorted(G.nodes())
    edges = list(G.edges())
    m = len(edges)

    strategies = {}
    # All permutations of [0..5] is 720, try all for small k
    for perm in itertools.permutations(range(k)):
        order = list(perm)
        strategies[f"bc_{order}"] = make_bounce_circular(order)
        strategies[f"co_{order}"] = make_circular(order)

    results = []

    for fail_size in range(1, max_fail + 1):
        for fc in itertools.combinations(range(m), fail_size):
            failure_set = set()
            for idx in fc:
                u, v = edges[idx]
                failure_set.add(frozenset({u, v}))

            H = G.copy()
            for fe in failure_set:
                u, v = tuple(fe)
                if H.has_edge(u, v):
                    H.remove_edge(u, v)
            if not nx.is_connected(H):
                continue

            for sname, strat in strategies.items():
                for source in nodes:
                    if source == root:
                        continue
                    delivered, looped = simulate(nodes, root, arbs, failure_set,
                                                 source, strat)
                    if not delivered:
                        results.append({
                            'strategy': sname,
                            'source': source,
                            'failures': [edges[i] for i in fc],
                            'looped': looped,
                        })
    return results


def main():
    rng = random.Random(12345)
    k = 6

    print("=" * 70)
    print("Phase 1: Sparse 6-connected graphs via edge removal from K_n")
    print("=" * 70)

    for n in [8, 9, 10]:
        print(f"\n--- n = {n} ---")
        for trial in range(10):
            G = generate_sparse_6connected(n, random.Random(rng.randint(0, 10**7)))
            m = G.number_of_edges()
            conn = nx.edge_connectivity(G)
            print(f"  Trial {trial}: m={m}, conn={conn}", end="")

            best_arbs = None
            best_shared = -1
            # Try many seeds to find arborescences with lots of sharing
            for seed in range(50):
                arbs = find_arborescences(G, 0, k, seed=seed)
                if arbs is None:
                    continue
                shared, total = analyze_arborescences(arbs)
                if shared > best_shared:
                    best_shared = shared
                    best_arbs = arbs

            if best_arbs is None:
                print(" - FAILED to find 6 arborescences")
                continue

            shared, total = analyze_arborescences(best_arbs)
            print(f", shared_edges={shared}/{total}", end="")

            # For small graphs, do exhaustive test with a sample of orderings
            if m <= 24:
                print(" [exhaustive]", end="")
                results = test_exhaustive(G, 0, best_arbs, k, max_fail=5)
                loops = [r for r in results if r['looped']]
                print(f" -> {len(loops)} loops, {len(results)} total failures")
                if loops:
                    # Print first few
                    for r in loops[:3]:
                        print(f"    LOOP: strat={r['strategy'][:30]} "
                              f"src={r['source']} fail={r['failures']}")
            else:
                # Sample test
                print(" [sampled]", end="")
                edges = list(G.edges())
                loop_count = 0
                tested = 0
                strats = {}
                for perm in [[0,3,1,4,2,5], [0,1,2,3,4,5], [0,2,4,1,3,5]]:
                    strats[f"bc_{perm}"] = make_bounce_circular(perm)
                    strats[f"co_{perm}"] = make_circular(perm)
                for _ in range(5000):
                    fc = tuple(sorted(rng.sample(range(m), min(5, m))))
                    failure_set = set()
                    for idx in fc:
                        u, v = edges[idx]
                        failure_set.add(frozenset({u, v}))
                    H = G.copy()
                    for fe in failure_set:
                        u, v = tuple(fe)
                        if H.has_edge(u, v):
                            H.remove_edge(u, v)
                    if not nx.is_connected(H):
                        continue
                    tested += 1
                    for sn, st in strats.items():
                        for src in G.nodes():
                            if src == 0:
                                continue
                            d, l = simulate(sorted(G.nodes()), 0, best_arbs,
                                            failure_set, src, st)
                            if l:
                                loop_count += 1
                print(f" -> {loop_count} loops in {tested} tests")

    print("\n" + "=" * 70)
    print("Phase 2: Near-6-regular graphs")
    print("=" * 70)

    for n in [8, 10, 12, 14]:
        print(f"\n--- n = {n} (6-regular) ---")
        for trial in range(20):
            G = generate_near_6regular(n, random.Random(rng.randint(0, 10**7)))
            if G is None:
                continue
            m = G.number_of_edges()
            print(f"  Trial {trial}: m={m}", end="")

            best_arbs = None
            best_shared = -1
            for seed in range(30):
                arbs = find_arborescences(G, 0, k, seed=seed)
                if arbs is None:
                    continue
                shared, total = analyze_arborescences(arbs)
                if shared > best_shared:
                    best_shared = shared
                    best_arbs = arbs

            if best_arbs is None:
                print(" - no arbs found")
                continue

            shared, total = analyze_arborescences(best_arbs)
            print(f", shared={shared}/{total}", end="")

            edges = list(G.edges())
            loop_count = 0
            tested = 0
            strats = {}
            for perm in [[0,3,1,4,2,5], [0,1,2,3,4,5]]:
                strats[f"bc_{perm}"] = make_bounce_circular(perm)
                strats[f"co_{perm}"] = make_circular(perm)
            for _ in range(3000):
                fc = tuple(sorted(rng.sample(range(m), 5)))
                failure_set = set()
                for idx in fc:
                    u, v = edges[idx]
                    failure_set.add(frozenset({u, v}))
                H = G.copy()
                for fe in failure_set:
                    u, v = tuple(fe)
                    if H.has_edge(u, v):
                        H.remove_edge(u, v)
                if not nx.is_connected(H):
                    continue
                tested += 1
                for sn, st in strats.items():
                    for src in G.nodes():
                        if src == 0:
                            continue
                        d, l = simulate(sorted(G.nodes()), 0, best_arbs,
                                        failure_set, src, st)
                        if l:
                            loop_count += 1
            print(f" -> {loop_count} loops in {tested} tests")


if __name__ == '__main__':
    main()

#!/usr/bin/env python3
"""
Search v3: Exhaustive AND-OR reachability on small multigraphs.

For a SPECIFIC failure set, AND-OR reachability checks whether there EXISTS
a forwarding choice at each vertex that delivers all sources.

If AND-OR reachability fails for some failure set, the conjecture fails.
If it holds for all failure sets, we additionally check strategy consistency.
"""

import itertools
from collections import defaultdict


class Multigraph:
    """Simple multigraph with labeled edges."""
    def __init__(self, n):
        self.n = n
        self.edges = []  # list of (u, v, label)

    def add_edge(self, u, v, label):
        self.edges.append((u, v, label))

    def incident(self, v):
        """Return edges incident to v."""
        return [(u, w, l) for u, w, l in self.edges if u == v or w == v]


def make_4vertex_6connected():
    """
    4 vertices {0,1,2,3}, root=0.
    2 edges between each pair = 12 edges.
    This is 6-edge-connected.
    """
    G = Multigraph(4)
    for u, v in itertools.combinations(range(4), 2):
        G.add_edge(u, v, 'a')
        G.add_edge(u, v, 'b')
    return G


def make_3vertex_6connected():
    """
    3 vertices {0,1,2}, root=0.
    3 edges between each pair = 9 edges.
    This is 6-edge-connected.
    """
    G = Multigraph(3)
    for u, v in itertools.combinations(range(3), 2):
        for label in ['a', 'b', 'c']:
            G.add_edge(u, v, label)
    return G


def construct_arborescences_4v():
    """
    Manually construct 6 arc-disjoint arborescences for 4-vertex multigraph.
    Each arb maps vertex -> (parent, edge_label), with root -> None.
    Arc = (v, parent, label) directed toward root.
    """
    # T1: star via vertex 1, using 'a' edges to root
    # 1->0(a), 2->1(a), 3->1(a)
    T1 = {0: None, 1: (0, 'a'), 2: (1, 'a'), 3: (1, 'a')}
    # T2: star via vertex 2
    T2 = {0: None, 2: (0, 'a'), 1: (2, 'a'), 3: (2, 'a')}
    # T3: star via vertex 3
    T3 = {0: None, 3: (0, 'a'), 1: (3, 'a'), 2: (3, 'a')}
    # T4: star via vertex 1, using 'b' edges
    T4 = {0: None, 1: (0, 'b'), 2: (1, 'b'), 3: (1, 'b')}
    # T5: star via vertex 2, 'b' edges
    T5 = {0: None, 2: (0, 'b'), 1: (2, 'b'), 3: (2, 'b')}
    # T6: star via vertex 3, 'b' edges
    T6 = {0: None, 3: (0, 'b'), 1: (3, 'b'), 2: (3, 'b')}

    # Verify arc-disjointness
    all_arcs = set()
    for i, T in enumerate([T1, T2, T3, T4, T5, T6]):
        for v, info in T.items():
            if info is not None:
                parent, label = info
                arc = (v, parent, label)
                assert arc not in all_arcs, f"Duplicate arc {arc} in T{i+1}"
                all_arcs.add(arc)

    return [T1, T2, T3, T4, T5, T6]


def construct_arborescences_3v():
    """
    Manually construct 6 arc-disjoint arborescences for 3-vertex multigraph.
    Vertices: 0 (root), 1, 2. Each pair connected by 3 edges (a, b, c).
    Symmetric digraph has 18 arcs. Need 6 arbs × 2 arcs = 12 arcs.
    """
    # Each arb needs: 1 -> ? -> 0, 2 -> ? -> 0 (paths of length 1 or 2)
    # Direct arcs to 0: (1,0,a), (1,0,b), (1,0,c), (2,0,a), (2,0,b), (2,0,c) = 6 arcs
    # Between 1,2: (1,2,a), (1,2,b), (1,2,c), (2,1,a), (2,1,b), (2,1,c) = 6 arcs
    # From 0: (0,1,*), (0,2,*) = 6 arcs (not useful for arborescences toward 0)

    # T1: 1->0(a), 2->0(a)
    T1 = {0: None, 1: (0, 'a'), 2: (0, 'a')}
    # T2: 1->0(b), 2->0(b)
    T2 = {0: None, 1: (0, 'b'), 2: (0, 'b')}
    # T3: 1->0(c), 2->0(c)
    T3 = {0: None, 1: (0, 'c'), 2: (0, 'c')}
    # T4: 1->2(a), 2->0 -- but (2,0,*) all used! Need to use a chain.
    # Wait, all direct (v,0) arcs used by T1-T3.
    # T4: 2->1(a), 1->0 -- but (1,0,*) all used!
    # Hmm, can't make T4 with 3-vertex graph if all direct arcs to root are used.

    # Let me reconsider. 6 arcs to root exist. 6 arborescences each need 2 arcs.
    # Each arb needs at least 1 "to root" arc. With 6 "to root" arcs and 6 arbs,
    # each arb uses exactly 1 "to root" arc. The other arc goes 1->2 or 2->1.

    T1 = {0: None, 1: (0, 'a'), 2: (1, 'a')}  # 2->1(a)->0(a)
    T2 = {0: None, 2: (0, 'a'), 1: (2, 'a')}  # 1->2(a)->0(a)
    T3 = {0: None, 1: (0, 'b'), 2: (1, 'b')}  # 2->1(b)->0(b)
    T4 = {0: None, 2: (0, 'b'), 1: (2, 'b')}  # 1->2(b)->0(b)
    T5 = {0: None, 1: (0, 'c'), 2: (1, 'c')}  # 2->1(c)->0(c)
    T6 = {0: None, 2: (0, 'c'), 1: (2, 'c')}  # 1->2(c)->0(c)

    all_arcs = set()
    for i, T in enumerate([T1, T2, T3, T4, T5, T6]):
        for v, info in T.items():
            if info is not None:
                parent, label = info
                arc = (v, parent, label)
                assert arc not in all_arcs, f"Dup arc {arc} in T{i+1}"
                all_arcs.add(arc)

    return [T1, T2, T3, T4, T5, T6]


def check_and_or_reachability(n, root, arbs, failure_set):
    """
    Check AND-OR reachability for all sources to root.

    For states (v, arb_i) where arb_i's arc at v is active:
        deterministic transition.
    For states (v, arb_i) where arb_i's arc at v is failed:
        choice among non-failed arborescences.

    Returns dict: source -> bool (reachable or not).
    """
    k = len(arbs)

    # Build arc info
    out_arc = {}  # (v, i) -> (parent, label)
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                out_arc[(v, i)] = info

    # Determine failed arcs
    failed_arcs = set()
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                edge = (min(v, parent), max(v, parent), label)
                if edge in failure_set:
                    failed_arcs.add((v, i))

    # Backward induction: find all "good" states
    good = set()
    for i in range(k):
        good.add((root, i))

    changed = True
    while changed:
        changed = False
        for v in range(n):
            if v == root:
                continue
            for i in range(k):
                if (v, i) in good:
                    continue
                if (v, i) not in failed_arcs:
                    # Active arc: deterministic
                    parent, label = out_arc[(v, i)]
                    # After forwarding, packet is at parent on arb i
                    if (parent, i) in good:
                        good.add((v, i))
                        changed = True
                else:
                    # Failed arc: choice - try all non-failed arbs
                    for j in range(k):
                        if j == i:
                            continue
                        if (v, j) in failed_arcs:
                            continue
                        if (v, j) not in out_arc:
                            continue
                        parent_j, label_j = out_arc[(v, j)]
                        if (parent_j, j) in good:
                            good.add((v, i))
                            changed = True
                            break

    # Check reachability for each source
    result = {}
    for src in range(n):
        if src == root:
            result[src] = True
            continue
        # Source can start on ANY arborescence
        reachable = any((src, i) in good for i in range(k))
        result[src] = reachable

    return result


def edge_key(u, v, label):
    return (min(u, v), max(u, v), label)


def check_connectivity_after_failures(n, edges, failure_set):
    """Check if graph remains connected after removing failed edges."""
    adj = defaultdict(set)
    active_edges = set()
    for u, v, l in edges:
        key = edge_key(u, v, l)
        if key not in failure_set:
            adj[u].add(v)
            adj[v].add(u)
            active_edges.add(key)

    if not active_edges:
        return False

    visited = set()
    queue = [0]
    visited.add(0)
    while queue:
        u = queue.pop()
        for v in adj[u]:
            if v not in visited:
                visited.add(v)
                queue.append(v)

    return len(visited) == n


def analyze_graph(name, n, edges, arbs, max_failures):
    """Full analysis of a graph."""
    k = len(arbs)
    print(f"\n{'='*60}")
    print(f"Analyzing: {name}")
    print(f"  Vertices: {n}, Edges: {len(edges)}, Arborescences: {k}")

    # Analyze sharing
    arc_edge_map = {}  # (v, parent, label) -> arb_index
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                arc_edge_map[(v, parent, label)] = i

    shared_count = 0
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                reverse = (parent, v, label)
                if reverse in arc_edge_map and arc_edge_map[reverse] != i:
                    shared_count += 1

    print(f"  Shared arcs: {shared_count} (arcs whose reverse is in another arb)")

    # Enumerate all failure sets
    edge_keys = list(set(edge_key(u, v, l) for u, v, l in edges))
    num_edges = len(edge_keys)
    print(f"  Distinct edges: {num_edges}")

    unreachable_cases = []
    total_tested = 0

    for fail_size in range(1, min(max_failures + 1, num_edges + 1)):
        for fc in itertools.combinations(range(num_edges), fail_size):
            failure_set = set(edge_keys[i] for i in fc)

            # Check connectivity
            if not check_connectivity_after_failures(n, edges, failure_set):
                continue

            total_tested += 1
            reachability = check_and_or_reachability(n, 0, arbs, failure_set)

            for src, reachable in reachability.items():
                if src != 0 and not reachable:
                    failed_edges = [edge_keys[i] for i in fc]
                    unreachable_cases.append({
                        'source': src,
                        'failures': failed_edges,
                        'fail_size': fail_size,
                    })

    print(f"  Total failure sets tested: {total_tested}")
    print(f"  Unreachable cases (AND-OR): {len(unreachable_cases)}")

    if unreachable_cases:
        print(f"\n  *** CONJECTURE FAILS FOR THIS GRAPH! ***")
        print(f"  No BSC strategy can handle these failure sets:")
        for case in unreachable_cases[:10]:
            print(f"    Source {case['source']}, failures: {case['failures']}")
        if len(unreachable_cases) > 10:
            print(f"    ... and {len(unreachable_cases) - 10} more")
    else:
        print(f"  AND-OR reachability holds for all failure sets.")
        print(f"  The conjecture is consistent with this graph.")


def main():
    # Test 1: 3-vertex multigraph (3 edges per pair)
    G3 = make_3vertex_6connected()
    arbs3 = construct_arborescences_3v()
    analyze_graph(
        "3-vertex 6-connected multigraph (3 edges per pair)",
        3, G3.edges, arbs3, max_failures=5
    )

    # Test 2: 4-vertex multigraph (2 edges per pair)
    G4 = make_4vertex_6connected()
    arbs4 = construct_arborescences_4v()
    analyze_graph(
        "4-vertex 6-connected multigraph (2 edges per pair)",
        4, G4.edges, arbs4, max_failures=5
    )

    # Test 3: Try different arborescence constructions for 4-vertex graph
    # Chain-style arborescences
    T1 = {0: None, 1: (0, 'a'), 2: (1, 'a'), 3: (2, 'a')}  # 3->2->1->0
    T2 = {0: None, 2: (0, 'a'), 3: (2, 'b'), 1: (3, 'a')}  # 1->3->2->0
    T3 = {0: None, 3: (0, 'a'), 1: (3, 'b'), 2: (1, 'b')}  # 2->1->3->0
    T4 = {0: None, 1: (0, 'b'), 3: (1, 'a'), 2: (3, 'b')}  # 2->3->1->0
    T5 = {0: None, 2: (0, 'b'), 1: (2, 'b'), 3: (1, 'b')}  # 3->1->2->0
    T6 = {0: None, 3: (0, 'b'), 2: (3, 'a'), 1: (2, 'a')}  # wait, (2,3,a) might clash

    # Verify arc-disjointness
    all_arcs = set()
    valid = True
    for i, T in enumerate([T1, T2, T3, T4, T5, T6]):
        for v, info in T.items():
            if info is not None:
                parent, label = info
                arc = (v, parent, label)
                if arc in all_arcs:
                    print(f"  Clash: arc {arc} in T{i+1}")
                    valid = False
                all_arcs.add(arc)

    if valid:
        analyze_graph(
            "4-vertex, chain-style arborescences",
            4, G4.edges, [T1, T2, T3, T4, T5, T6], max_failures=5
        )
    else:
        print("\nChain-style arborescences have clashes, trying to fix...")
        # Try a different chain construction
        T1 = {0: None, 1: (0, 'a'), 2: (1, 'a'), 3: (2, 'a')}
        T2 = {0: None, 2: (0, 'a'), 1: (2, 'a'), 3: (1, 'a')}
        # Check clash: T1 has (2,1,a), T2 has (1,2,a). Different arcs. OK.
        # T1 has (3,2,a), T2 has (3,1,a). Different arcs. OK.
        T3 = {0: None, 3: (0, 'a'), 2: (3, 'a'), 1: (2, 'b')}
        T4 = {0: None, 1: (0, 'b'), 3: (1, 'b'), 2: (3, 'b')}
        T5 = {0: None, 2: (0, 'b'), 3: (2, 'b'), 1: (3, 'b')}
        T6 = {0: None, 3: (0, 'b'), 1: (3, 'a'), 2: (1, 'b')}

        all_arcs2 = set()
        valid2 = True
        for i, T in enumerate([T1, T2, T3, T4, T5, T6]):
            for v, info in T.items():
                if info is not None:
                    parent, label = info
                    arc = (v, parent, label)
                    if arc in all_arcs2:
                        print(f"  Clash: arc {arc} in T{i+1}")
                        valid2 = False
                    all_arcs2.add(arc)

        if valid2:
            analyze_graph(
                "4-vertex, mixed arborescences (v2)",
                4, G4.edges, [T1, T2, T3, T4, T5, T6], max_failures=5
            )
        else:
            print("  Still clashing, skipping.")

    print("\n" + "=" * 60)
    print("SUMMARY")
    print("=" * 60)
    print("If no 'CONJECTURE FAILS' message appeared above,")
    print("then AND-OR reachability holds for all tested graphs,")
    print("meaning the conjecture is consistent with these examples.")


if __name__ == '__main__':
    main()

#!/usr/bin/env python3
"""
Search for counterexamples to BSC (k-1)-resilient forwarding for k=12.

Key insight: k=12 means we need 12-connected graphs, 12 arc-disjoint
arborescences, and must tolerate 11 failures. The larger k makes it
harder for BSC strategies to find the good arborescence.

We use:
1. Small multigraphs where we can manually construct arborescences
2. AND-OR reachability to check if ANY BSC strategy can fail
3. Explicit strategy simulation for specific strategies
"""

import itertools
import random
from collections import defaultdict


def edge_key(u, v, label):
    return (min(u, v), max(u, v), label)


def check_connectivity(n, edges, failure_set):
    """Check if graph remains connected after failures."""
    adj = defaultdict(set)
    for u, v, l in edges:
        key = edge_key(u, v, l)
        if key not in failure_set:
            adj[u].add(v)
            adj[v].add(u)
    visited = set()
    queue = [0]
    visited.add(0)
    while queue:
        u = queue.pop()
        for v in adj[u]:
            if v not in visited:
                visited.add(v)
                queue.append(v)
    return len(visited) == n


def check_and_or_reachability(n, root, arbs, failure_set):
    """
    AND-OR reachability: can ALL sources reach root under SOME BSC choice?

    Returns dict: source -> bool.
    """
    k = len(arbs)
    out_arc = {}
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                out_arc[(v, i)] = info

    failed_arcs = set()
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                e = edge_key(v, parent, label)
                if e in failure_set:
                    failed_arcs.add((v, i))

    good = set()
    for i in range(k):
        good.add((root, i))

    changed = True
    while changed:
        changed = False
        for v in range(n):
            if v == root:
                continue
            for i in range(k):
                if (v, i) in good:
                    continue
                if (v, i) not in failed_arcs:
                    # Active arc: deterministic transition
                    if (v, i) in out_arc:
                        parent, label = out_arc[(v, i)]
                        if (parent, i) in good:
                            good.add((v, i))
                            changed = True
                else:
                    # Failed arc: existential choice
                    for j in range(k):
                        if j == i or (v, j) in failed_arcs:
                            continue
                        if (v, j) not in out_arc:
                            continue
                        parent_j, _ = out_arc[(v, j)]
                        if (parent_j, j) in good:
                            good.add((v, i))
                            changed = True
                            break

    result = {}
    for src in range(n):
        if src == root:
            result[src] = True
        else:
            result[src] = any((src, i) in good for i in range(k))
    return result


def make_multigraph_and_arbs(num_vertices, k):
    """
    Construct a k-connected multigraph on num_vertices vertices and
    k arc-disjoint arborescences.

    Strategy: put ceil(k / (num_vertices-1)) edges between each pair,
    then construct arborescences as stars through each non-root vertex.
    """
    n = num_vertices
    root = 0
    non_root = list(range(1, n))
    num_non_root = n - 1

    # Each arborescence is a star: all non-root vertices route through
    # one "hub" vertex to the root. The hub uses a direct arc to root,
    # other vertices use arcs to the hub.

    # We need k arborescences. Group them by hub vertex.
    # With (n-1) possible hubs, we need ceil(k/(n-1)) copies per hub.
    copies_per_hub = (k + num_non_root - 1) // num_non_root

    # Edges needed:
    # - Between each non-root vertex and root: copies_per_hub edges
    #   (one per arborescence that uses this vertex as hub)
    # - Between each pair of non-root vertices: copies_per_hub edges
    #   (one per arborescence where one is hub and other routes through it)

    # Actually, let's be more precise. For hub vertex h:
    # - Arc (h, root, label): one per arborescence using h as hub
    # - Arc (v, h, label) for each other non-root v: one per arborescence

    # Number of labels needed per pair:
    edges = []
    arbs = []
    label_counters = defaultdict(int)  # (min(u,v), max(u,v)) -> count

    def next_label(u, v):
        key = (min(u, v), max(u, v))
        c = label_counters[key]
        label_counters[key] += 1
        return str(c)

    arb_idx = 0
    for hub in non_root:
        for copy in range(copies_per_hub):
            if arb_idx >= k:
                break
            arb = {root: None}
            # Hub -> root
            lbl = next_label(hub, root)
            arb[hub] = (root, lbl)
            edges.append((hub, root, lbl))
            # Other non-root -> hub
            for v in non_root:
                if v == hub:
                    continue
                lbl2 = next_label(v, hub)
                arb[v] = (hub, lbl2)
                edges.append((v, hub, lbl2))
            arbs.append(arb)
            arb_idx += 1
        if arb_idx >= k:
            break

    if arb_idx < k:
        return None, None, None

    # Verify arc-disjointness
    all_arcs = set()
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                arc = (v, parent, label)
                if arc in all_arcs:
                    return None, None, None
                all_arcs.add(arc)

    # Add reverse edges to make the undirected graph k-connected
    # (we need k edge-disjoint paths between every pair)
    # The star construction already gives enough connectivity if we have
    # enough edge copies. Let's also add edges between non-root pairs
    # that aren't yet present to boost connectivity.
    existing_edge_keys = set(edge_key(u, v, l) for u, v, l in edges)

    # Check edge connectivity
    n_vertices = n
    # Build undirected adjacency for connectivity check
    def compute_edge_connectivity():
        adj = defaultdict(list)
        edge_list = []
        for u, v, l in edges:
            ek = edge_key(u, v, l)
            if ek not in set(e for e in edge_list):
                edge_list.append(ek)
                adj[u].append((v, len(edge_list)-1))
                adj[v].append((u, len(edge_list)-1))
        # Simple min-cut via max-flow between all pairs
        min_conn = float('inf')
        for s in range(n_vertices):
            for t in range(s+1, n_vertices):
                # BFS-based max flow with unit capacities
                flow = 0
                used_edges = set()
                while True:
                    # BFS find augmenting path
                    parent = {s: (-1, -1)}
                    queue = [s]
                    found = False
                    while queue and not found:
                        u = queue.pop(0)
                        for v, eidx in adj[u]:
                            if v not in parent and eidx not in used_edges:
                                parent[v] = (u, eidx)
                                if v == t:
                                    found = True
                                    break
                                queue.append(v)
                    if not found:
                        break
                    # Trace path and mark edges
                    v = t
                    while v != s:
                        u, eidx = parent[v]
                        used_edges.add(eidx)
                        v = u
                    flow += 1
                min_conn = min(min_conn, flow)
        return min_conn

    conn = compute_edge_connectivity()

    return edges, arbs, conn


def analyze_sampled(name, n, edges, arbs, k, max_failures, num_samples=50000):
    """Analyze using sampled failure sets."""
    print(f"\n{'='*60}")
    print(f"Analyzing: {name}")
    print(f"  n={n}, edges={len(edges)}, k={k}, max_failures={max_failures}")

    # Count shared arcs
    arc_to_arb = {}
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                arc_to_arb[(v, parent, label)] = i

    shared = 0
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                rev = (parent, v, label)
                if rev in arc_to_arb and arc_to_arb[rev] != i:
                    shared += 1

    edge_keys = list(set(edge_key(u, v, l) for u, v, l in edges))
    num_edges = len(edge_keys)
    print(f"  Distinct edges: {num_edges}, shared arcs: {shared}")

    if num_edges < max_failures:
        print(f"  Not enough edges for {max_failures} failures, skipping")
        return

    rng = random.Random(42)
    unreachable_count = 0
    tested = 0

    # If small enough, enumerate exhaustively
    total_combos = 1
    for i in range(max_failures):
        total_combos = total_combos * (num_edges - i) // (i + 1)

    if total_combos <= 200000:
        print(f"  Exhaustive enumeration ({total_combos} combinations)")
        iterator = itertools.combinations(range(num_edges), max_failures)
    else:
        print(f"  Sampling {num_samples} failure sets "
              f"(out of ~{total_combos})")
        def sampler():
            seen = set()
            for _ in range(num_samples):
                fc = tuple(sorted(rng.sample(range(num_edges), max_failures)))
                if fc not in seen:
                    seen.add(fc)
                    yield fc
        iterator = sampler()

    for fc in iterator:
        failure_set = set(edge_keys[i] for i in fc)

        if not check_connectivity(n, edges, failure_set):
            continue

        tested += 1
        reachability = check_and_or_reachability(n, 0, arbs, failure_set)

        for src, reachable in reachability.items():
            if src != 0 and not reachable:
                unreachable_count += 1
                if unreachable_count <= 5:
                    failed = [edge_keys[i] for i in fc]
                    print(f"  *** UNREACHABLE: src={src}, "
                          f"failures={failed}")

    print(f"  Tested: {tested} valid failure sets")
    print(f"  Unreachable cases: {unreachable_count}")

    if unreachable_count > 0:
        print(f"  >>> CONJECTURE FAILS! No BSC strategy works. <<<")
    else:
        print(f"  AND-OR reachability holds. Conjecture consistent.")


def main():
    k = 12
    max_failures = k - 1  # = 11

    print(f"Searching for counterexamples: k={k}, max_failures={max_failures}")
    print(f"Need {k}-connected graphs with {k} arc-disjoint arborescences")

    # Test 1: 3-vertex multigraph
    # With 3 vertices (root + 2), each arb is a star through one of the 2
    # non-root vertices. Need 12 arbs = 6 per hub.
    # Each hub needs 6 direct edges to root and each other vertex needs
    # 6 edges to the hub. So 6 edges per pair × 3 pairs = 18 edges.
    # But we only have 2 non-root vertices, so 6 copies through hub 1
    # and 6 through hub 2.
    print("\n--- 3-vertex multigraph ---")
    edges3, arbs3, conn3 = make_multigraph_and_arbs(3, k)
    if edges3 and conn3 >= k:
        analyze_sampled(f"3-vertex, conn={conn3}", 3, edges3, arbs3, k,
                        max_failures)
    elif edges3:
        print(f"  Connectivity only {conn3}, need {k}. Adding edges...")
        # Add more edges to boost connectivity
        label_ctr = defaultdict(int)
        for u, v, l in edges3:
            key = (min(u, v), max(u, v))
            label_ctr[key] = max(label_ctr[key], int(l) + 1)
        while conn3 < k:
            # Add edge between least-connected pair
            for u in range(3):
                for v in range(u+1, 3):
                    key = (u, v)
                    lbl = str(label_ctr[key])
                    label_ctr[key] += 1
                    edges3.append((u, v, lbl))
                    _, _, conn3 = make_multigraph_and_arbs(3, k)
                    break
                break
            # Recompute connectivity
            break
        if conn3 >= k:
            analyze_sampled(f"3-vertex augmented, conn={conn3}", 3, edges3,
                            arbs3, k, max_failures)
        else:
            print(f"  Still only conn={conn3}, proceeding anyway")
            analyze_sampled(f"3-vertex, conn={conn3}", 3, edges3, arbs3, k,
                            max_failures)

    # Test 2: 4-vertex multigraph
    print("\n--- 4-vertex multigraph ---")
    edges4, arbs4, conn4 = make_multigraph_and_arbs(4, k)
    if edges4:
        analyze_sampled(f"4-vertex, conn={conn4}", 4, edges4, arbs4, k,
                        max_failures)

    # Test 3: 5-vertex multigraph
    print("\n--- 5-vertex multigraph ---")
    edges5, arbs5, conn5 = make_multigraph_and_arbs(5, k)
    if edges5:
        analyze_sampled(f"5-vertex, conn={conn5}", 5, edges5, arbs5, k,
                        max_failures)

    # Test 4: 7-vertex multigraph (k/2 + 1 = 7 non-root, 2 copies each)
    print("\n--- 7-vertex multigraph ---")
    edges7, arbs7, conn7 = make_multigraph_and_arbs(7, k)
    if edges7:
        analyze_sampled(f"7-vertex, conn={conn7}", 7, edges7, arbs7, k,
                        max_failures)

    # Test 5: 13-vertex multigraph (k+1 vertices, 1 arb per hub)
    print("\n--- 13-vertex multigraph ---")
    edges13, arbs13, conn13 = make_multigraph_and_arbs(13, k)
    if edges13:
        analyze_sampled(f"13-vertex, conn={conn13}", 13, edges13, arbs13, k,
                        max_failures, num_samples=100000)

    print(f"\n{'='*60}")
    print("DONE")


if __name__ == '__main__':
    main()

#!/usr/bin/env python3
"""
k=12 search with CHAIN arborescences that maximize edge sharing.

Key: star arborescences have 0 shared edges. Chain arborescences share
every non-root edge with exactly one other arborescence, creating the
bounce dynamics that make BSC hard.

4-vertex multigraph with 4 labels per edge pair = 24 edges.
12 chain arborescences, all non-root arcs shared.
"""

import itertools
import random
from collections import defaultdict


def edge_key(u, v, label):
    return (min(u, v), max(u, v), label)


def build_chain_arborescences_k12():
    """
    4 vertices {0,1,2,3}, root=0.
    4 labels per edge pair (a,b,c,d) = 24 undirected edges.
    12 chain arborescences with maximum sharing.

    Each chain arborescence is a directed path of length 3 toward root 0.
    Six chain structures on 4 vertices toward root 0:
      C_type1: 3->2->1->0    C_type2: 2->3->1->0
      C_type3: 3->1->2->0    C_type4: 1->3->2->0
      C_type5: 2->1->3->0    C_type6: 1->2->3->0

    Using labels a,b for group 1 (6 arbs) and c,d for group 2 (6 arbs).
    """
    n = 4
    root = 0
    edges = []

    # Add 4 copies of each of the 6 edge pairs
    for u, v in itertools.combinations(range(4), 2):
        for label in ['a', 'b', 'c', 'd']:
            edges.append((u, v, label))

    # Group 1: labels a, b
    # Each chain type uses one "root arc" and two "internal arcs"
    CA1 = {0: None, 3: (2, 'a'), 2: (1, 'a'), 1: (0, 'a')}  # 3->2(a)->1(a)->0(a)
    CA2 = {0: None, 2: (3, 'a'), 3: (1, 'a'), 1: (0, 'b')}  # 2->3(a)->1(a)->0(b)
    CA3 = {0: None, 3: (1, 'b'), 1: (2, 'a'), 2: (0, 'a')}  # 3->1(b)->2(a)->0(a)
    CA4 = {0: None, 1: (3, 'a'), 3: (2, 'b'), 2: (0, 'b')}  # 1->3(a)->2(b)->0(b)
    CA5 = {0: None, 2: (1, 'b'), 1: (3, 'b'), 3: (0, 'a')}  # 2->1(b)->3(b)->0(a)
    CA6 = {0: None, 1: (2, 'b'), 2: (3, 'b'), 3: (0, 'b')}  # 1->2(b)->3(b)->0(b)

    # Group 2: labels c, d (same structure, different labels)
    CB1 = {0: None, 3: (2, 'c'), 2: (1, 'c'), 1: (0, 'c')}
    CB2 = {0: None, 2: (3, 'c'), 3: (1, 'c'), 1: (0, 'd')}
    CB3 = {0: None, 3: (1, 'd'), 1: (2, 'c'), 2: (0, 'c')}
    CB4 = {0: None, 1: (3, 'c'), 3: (2, 'd'), 2: (0, 'd')}
    CB5 = {0: None, 2: (1, 'd'), 1: (3, 'd'), 3: (0, 'c')}
    CB6 = {0: None, 1: (2, 'd'), 2: (3, 'd'), 3: (0, 'd')}

    arbs = [CA1, CA2, CA3, CA4, CA5, CA6, CB1, CB2, CB3, CB4, CB5, CB6]

    # Verify arc-disjointness
    all_arcs = set()
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                arc = (v, parent, label)
                assert arc not in all_arcs, \
                    f"Duplicate arc {arc} in arb {i}"
                all_arcs.add(arc)

    print(f"Total arcs used: {len(all_arcs)} (of 48 available)")

    # Analyze sharing
    arc_to_arb = {}
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                arc_to_arb[(v, parent, label)] = i

    shared_count = 0
    shared_pairs = []
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                rev = (parent, v, label)
                if rev in arc_to_arb:
                    j = arc_to_arb[rev]
                    if j != i:
                        shared_count += 1
                        shared_pairs.append((i, j, v, parent, label))

    print(f"Shared arcs: {shared_count}")
    print(f"Sharing pairs:")
    for i, j, v, p, l in shared_pairs:
        print(f"  Arb{i}({v}->{p},{l}) <-> Arb{j}({p}->{v},{l})")

    return n, edges, arbs


def check_connectivity(n, edges, failure_set):
    adj = defaultdict(set)
    for u, v, l in edges:
        if edge_key(u, v, l) not in failure_set:
            adj[u].add(v)
            adj[v].add(u)
    visited = set()
    queue = [0]
    visited.add(0)
    while queue:
        u = queue.pop()
        for v in adj[u]:
            if v not in visited:
                visited.add(v)
                queue.append(v)
    return len(visited) == n


def check_and_or_reachability(n, root, arbs, failure_set):
    k = len(arbs)
    out_arc = {}
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                out_arc[(v, i)] = info

    failed_arcs = set()
    for i, arb in enumerate(arbs):
        for v, info in arb.items():
            if info is not None:
                parent, label = info
                if edge_key(v, parent, label) in failure_set:
                    failed_arcs.add((v, i))

    good = set()
    for i in range(k):
        good.add((root, i))

    changed = True
    while changed:
        changed = False
        for v in range(n):
            if v == root:
                continue
            for i in range(k):
                if (v, i) in good:
                    continue
                if (v, i) not in failed_arcs:
                    if (v, i) in out_arc:
                        parent, _ = out_arc[(v, i)]
                        if (parent, i) in good:
                            good.add((v, i))
                            changed = True
                else:
                    for j in range(k):
                        if j == i or (v, j) in failed_arcs:
                            continue
                        if (v, j) not in out_arc:
                            continue
                        parent_j, _ = out_arc[(v, j)]
                        if (parent_j, j) in good:
                            good.add((v, i))
                            changed = True
                            break

    result = {}
    for src in range(n):
        if src == root:
            result[src] = True
        else:
            result[src] = any((src, i) in good for i in range(k))
    return result


def main():
    k = 12
    max_failures = k - 1  # 11

    print(f"k={k}, max_failures={max_failures}")
    print()

    n, edges, arbs = build_chain_arborescences_k12()

    edge_keys = list(set(edge_key(u, v, l) for u, v, l in edges))
    num_edges = len(edge_keys)
    print(f"\nGraph: {n} vertices, {num_edges} edges")

    # Compute total failure set combinations
    total = 1
    for i in range(max_failures):
        total = total * (num_edges - i) // (i + 1)
    print(f"Total failure sets of size {max_failures}: {total}")

    if total <= 500000:
        print("Exhaustive enumeration feasible!")
        iterator = itertools.combinations(range(num_edges), max_failures)
        mode = "exhaustive"
    else:
        num_samples = 500000
        print(f"Sampling {num_samples} failure sets")
        rng = random.Random(42)
        def sampler():
            seen = set()
            for _ in range(num_samples):
                fc = tuple(sorted(rng.sample(range(num_edges), max_failures)))
                if fc not in seen:
                    seen.add(fc)
                    yield fc
        iterator = sampler()
        mode = "sampled"

    tested = 0
    unreachable = 0
    unreachable_examples = []

    for fc in iterator:
        failure_set = set(edge_keys[i] for i in fc)
        if not check_connectivity(n, edges, failure_set):
            continue

        tested += 1
        reach = check_and_or_reachability(n, 0, arbs, failure_set)

        for src, ok in reach.items():
            if src != 0 and not ok:
                unreachable += 1
                if len(unreachable_examples) < 20:
                    unreachable_examples.append({
                        'source': src,
                        'failures': [edge_keys[i] for i in fc],
                    })

        if tested % 50000 == 0:
            print(f"  Progress: {tested} tested, {unreachable} unreachable")

    print(f"\nResults ({mode}):")
    print(f"  Failure sets tested: {tested}")
    print(f"  Unreachable cases: {unreachable}")

    if unreachable > 0:
        print(f"\n  *** CONJECTURE FAILS! ***")
        print(f"  No BSC strategy can handle these cases:")
        for ex in unreachable_examples:
            print(f"    Source {ex['source']}: fail {ex['failures']}")
    else:
        print(f"\n  AND-OR reachability holds for all tested cases.")
        print(f"  Conjecture is consistent with this graph + arborescences.")


if __name__ == '__main__':
    main()

# Computational Complexity of Resilient Routing Table Construction

## Computing the Arborescences

The foundation for all approaches:

- Edmonds' algorithm finds $k$ arc-disjoint arborescences in $O(kn^2)$ or $O(knm)$ time. For $k=12$ vs $k=6$, this is just $2\times$ slower — linear scaling in $k$.
- The Lemma 3 edge-disjoint partition (Lovász splitting-off) is also polynomial. No qualitative difference between $k=6$ and $k=12$.

## Computing HDR Forwarding Tables (with $\lceil \log k \rceil$ header bits)

- Once arborescences are computed, the tables are deterministic: the algorithm (`HDR-Log-K`) directly specifies the forwarding rule at each vertex. Table size is $O(nk)$.
- Total: **polynomial**, $O(knm)$ dominated by arborescence computation. $k=12$ is roughly $2\times$ the work of $k=6$. No qualitative difference.

## Computing BSC Forwarding Tables (no header bits)

This is where things get interesting. There are three sub-problems:

| Problem | Complexity | $k=6$ vs $k=12$ |
|---|---|---|
| **Constructing** BSC tables (for $k \leq 5$) | Polynomial (direct construction) | N/A — only proven for $k \leq 5$ |
| **Verifying** that given BSC tables are $c$-resilient | coNP-complete in general | Harder for $k=12$ (more failure patterns) |
| **Finding** BSC tables that are $(k{-}1)$-resilient | Open (existence unproven for $k > 5$) | See below |

The verification result (coNP-completeness) is from Bentert, Ceylan-Kettler, Hübner, Schmid, and Srba (OPODIS 2025). They show that checking whether a given set of static rerouting rules provides "perfect resilience" (surviving all non-disconnecting failures) is coNP-complete. For $(k{-}1)$-resilience specifically, the input includes the failure bound, but the core hardness likely persists.

## Why $k=12$ is Qualitatively Harder than $k=6$ for BSC

The difficulty isn't in the arborescence computation — it's in the *strategy space* and *adversary space*:

1. **Adversary space**: The number of failure sets grows as $\binom{m}{k-1}$. For a graph with $m=100$ edges: $\binom{100}{5} \approx 7.5 \times 10^7$ for $k=6$, but $\binom{100}{11} \approx 1.0 \times 10^{13}$ for $k=12$. That's $10^5 \times$ more failure patterns to handle.

2. **Strategy space**: A BSC function at vertex $v$ with incoming arborescence $T_i$ must handle $2^{\deg(v)}$ possible active-edge configurations. For $k=12$ on a 12-connected graph, $\deg(v) \geq 12$, so at least $2^{12} = 4096$ configurations per $(v, T_i)$ pair, each requiring a forwarding choice. The total strategy space is roughly $k^{n \cdot k \cdot 2^{\deg}}$ — super-exponential.

3. **Proof technique**: For $k \leq 5$, the proofs work by exhaustive case analysis of how failures interact with arborescences. The number of cases grows super-exponentially with $k$. For $k=4$ the proof is already intricate (Theorem 4 in the paper); $k=5$ requires the full technical report. Extending this to $k=6$ would require analyzing all possible "bounce chains" — sequences of arborescence switches — which grow combinatorially. By $k=12$, this case analysis is completely infeasible by hand.

## What the Computational Search Showed

The AND-OR reachability check answered an *easier* question: for each failure set *independently*, does there exist *some* valid forwarding choice? This is polynomial per failure set (fixpoint computation on $O(nk)$ states). It found that the answer is always YES.

But the *hard* question is: does a *single* BSC function work for *all* failure sets simultaneously? This requires that the forwarding choice at $(v, T_i, \text{active\_edges})$ is *consistent* across all failure sets producing the same local view. This is a constraint satisfaction problem whose size scales with:
- Number of distinct local views: up to $O(nk \cdot 2^{\deg(v)})$
- Number of constraints: one per (failure set, source) pair

For $k=12$, both quantities are much larger than for $k=6$, making the consistency check exponentially harder.

## Summary

| | $k=6$ | $k=12$ |
|---|---|---|
| HDR table computation | ~$6nm$ | ~$12nm$ (2× slower) |
| BSC existence | Unproven | Unproven |
| BSC verification | coNP-complete | coNP-complete (larger instances) |
| Failure sets to survive | $\binom{m}{5}$ | $\binom{m}{11}$ (~$10^5\times$ more) |
| Case analysis complexity | Possibly feasible | Infeasible |

The bottom line: computing *HDR* tables scales linearly and is easy at any $k$. Computing *BSC* tables is a fundamentally different beast — not because of the arborescence computation, but because of the combinatorial explosion in the consistency requirement across exponentially many failure patterns. The gap between $k=6$ and $k=12$ is not just quantitative ($2\times$) but qualitative (the adversary and strategy spaces blow up super-exponentially).