"""Paper's literal weighted-incidence reduction and explicit SAT switch wiring."""
from dataclasses import dataclass
from itertools import product
from network import LiteralSource

SWITCH_ARCS=((0,9),(0,15),(1,17),(1,18),(2,8),(3,12),(8,5),(8,9),(9,10),(9,11),(10,8),(10,11),(11,6),(11,19),(12,13),(13,5),(13,14),(14,12),(14,15),(15,7),(15,16),(16,4),(16,10),(17,4),(17,18),(18,16),(18,19),(19,14),(19,17))
MODES={True:((0,15,16,4),(1,17,18,19,14,12,13,5),(2,8,9,10,11,6)),False:((0,9,11,19,17,4),(1,18,16,10,8,5),(3,12,13,14,15,7))}

@dataclass(frozen=True)
class DirectedLinkage:
    vertices:tuple
    arcs:tuple
    terminals:tuple  # a0,a1,b0,b1
    def __post_init__(self):
        if len(set(self.vertices))!=len(self.vertices) or len(self.terminals)!=4 or len(set(self.terminals))!=4 or any(v not in self.vertices for v in self.terminals) or any(u not in self.vertices or v not in self.vertices for u,v in self.arcs):raise ValueError('Distinct vertices and four distinct existing terminals required.')
    def reduced(self):
        a0,a1,b0,b1=self.terminals
        return DirectedLinkage(self.vertices,tuple((u,v) for u,v in self.arcs if u!=v and v not in [a0,a1] and u not in [b0,b1]),self.terminals)
    def source(self):
        g=self.reduced();a0,a1,b0,b1=g.terminals;internal=tuple(v for v in g.vertices if v not in g.terminals);rows=('boundary_source','boundary_sink')+internal
        if len(set(rows))!=len(rows):raise ValueError('Vertex names collide with reserved boundary row names.')
        idx={v:i for i,v in enumerate(internal,2)};L=[];P=[]
        for u,v in g.arcs:
            col=[0]*len(rows);tail=0 if u in [a0,a1] else idx[u];head=1 if v in [b0,b1] else idx[v]
            col[tail]=1 if u==a1 else -1;col[head]=(-1 if v==b0 else 1)*(2 if u==a1 else 1)*(2 if v==b1 else 1)
            L.append(tuple(max(-x,0) for x in col));P.append(tuple(max(x,0) for x in col))
        return LiteralSource(tuple(f'arc{i}:{u}->{v}' for i,(u,v) in enumerate(g.arcs)),rows,tuple(L),tuple(P))
    def path_certificate(self,paths):
        g=self.reduced();p,q=map(tuple,paths);a0,a1,b0,b1=g.terminals
        if not p or not q or (p[0],q[0],p[-1],q[-1])!=(a0,a1,b0,b1) or len(set(p))!=len(p) or len(set(q))!=len(q) or set(p)&set(q):raise ValueError('Desired vertex-disjoint simple paths required.')
        ids=[]
        for path in [p,q]:
            for edge in zip(path,path[1:]):
                if edge not in g.arcs:raise ValueError('Path contains a missing arc.')
                ids.append(g.arcs.index(edge))
        source=g.source();vertices=set(p+q)-set(g.terminals);S=[0,1]+[i for i,v in enumerate(source.reactions) if i>=2 and v in vertices]
        return source.certificate(sorted(ids),S)

def all_paths(arcs,start,end):
    adj={}
    for u,v in arcs:adj.setdefault(u,[]).append(v)
    result=[]
    def visit(path,seen):
        if path[-1]==end:result.append(tuple(path));return
        for v in adj.get(path[-1],[]):
            if v not in seen:visit(path+[v],seen|{v})
    visit([start],{start});return result

def switch_check():
    routes={(a,b):all_paths(SWITCH_ARCS,a,b) for a in range(4) for b in range(4,8)};controls=[];checks=0
    for a in range(4):
        for b in range(4,8):
            for p in routes[a,4]:
                for q in routes[1,b]:
                    if set(p)&set(q):continue
                    checks+=1
                    if (a,b)!=(0,5):raise ArithmeticError('Control port forcing failed.')
                    controls.append((p,q))
    residuals=[]
    for p,q in controls:
        used=set(p+q);available=[]
        for ports,paths in routes.items():
            if any(not used&set(path) for path in paths):available.append(ports)
        if any(ports not in [(2,6),(3,7)] for ports in available) or len(available)>1:raise ArithmeticError('Residual role/exclusivity failed.')
        residuals.append(available)
    for mode,(p,q,r) in MODES.items():
        if set(p)&set(q) or set(p)&set(r) or set(q)&set(r) or any(edge not in SWITCH_ARCS for path in [p,q,r] for edge in zip(path,path[1:])):raise ArithmeticError('Constructive switch witness failed.')
    return dict(vertices=20,arcs=len(SWITCH_ARCS),simple_port_paths=sum(map(len,routes.values())),control_pairs=len(controls),control_pair_checks=checks,residual_mode_counts={str(k):sum(k in a for a in residuals) for k in [(2,6),(3,7)]},all_three_properties=True,scope='Complete Python simple-path enumeration on the fixed 20-vertex gadget; independent finite replay, not a Lean kernel run.')

@dataclass(frozen=True)
class CNF:
    clauses:tuple
    variable_count:int
    def __post_init__(self):
        if type(self.variable_count)is not int or self.variable_count<0 or any(type(x)is not int or x==0 or abs(x)>self.variable_count for c in self.clauses for x in c):raise ValueError('Literals use signed one-based variable indices within the declared count.')
    def satisfied(self,assignment):
        if len(assignment)!=self.variable_count or any(type(x)is not bool for x in assignment):raise ValueError('A Boolean value for every variable is required.')
        return all(any(assignment[abs(x)-1]==(x>0) for x in c) for c in self.clauses)
    def assignments(self,budget=65536):
        for k,a in enumerate(product([False,True],repeat=self.variable_count)):
            if k>=budget:return dict(status='unknown_budget')
            if self.satisfied(a):return dict(status='sat',assignment=a)
        return dict(status='unsat_exhaustive')
    def compile(self):
        occurrences=[(j,x) for j,c in enumerate(self.clauses) for x in c];K=len(occurrences)+1;V=self.variable_count;switch=lambda i,p:f's{i}:{p}';rail=lambda j,b,k:f'h{j}:{b}:{k}';gate=lambda j:f'u{j}';clause=lambda j:f'd{j}'
        vertices=[switch(i,p) for i in range(K) for p in range(20)]+[gate(j) for j in range(V+1)]+[rail(j,b,k) for j in range(V) for b in range(2) for k in range(K+1)]+[clause(j) for j in range(len(self.clauses)+1)]
        arcs=[(switch(i,a),switch(i,b)) for i in range(K) for a,b in SWITCH_ARCS]
        for i in range(K-1):arcs.extend([(switch(i,5),switch(i+1,1)),(switch(i+1,4),switch(i,0))])
        arcs.append((switch(K-1,5),gate(0)))
        for j in range(V):
            for b in range(2):
                arcs.append((gate(j),rail(j,b,0)))
                for i in range(K):
                    if i<len(occurrences) and abs(occurrences[i][1])-1==j and (occurrences[i][1]>0)!=bool(b):arcs.extend([(rail(j,b,i),switch(i,3)),(switch(i,7),rail(j,b,i+1))])
                    else:arcs.append((rail(j,b,i),rail(j,b,i+1)))
                arcs.append((rail(j,b,K),gate(j+1)))
        arcs.append((gate(V),clause(0)))
        for i,(j,x) in enumerate(occurrences):arcs.extend([(clause(j),switch(i,2)),(switch(i,6),clause(j+1))])
        return DirectedLinkage(tuple(vertices),tuple(arcs),(switch(0,1),switch(K-1,0),clause(len(self.clauses)),switch(0,4)))
    def satisfying_paths(self,assignment):
        if not self.satisfied(assignment):raise ValueError('A satisfying assignment is required.')
        occurrences=[(j,x) for j,c in enumerate(self.clauses) for x in c];truth=[assignment[abs(x)-1]==(x>0) for j,x in occurrences]+[True];K=len(truth)
        P=[];Q=[]
        for i in range(K):P.extend(f's{i}:{p}' for p in MODES[truth[i]][1])
        for i in reversed(range(K)):Q.extend(f's{i}:{p}' for p in MODES[truth[i]][0])
        P.append('u0')
        for j,b in enumerate(assignment):
            P.append(f'h{j}:{int(b)}:0')
            for i in range(K):
                if i<len(occurrences) and abs(occurrences[i][1])-1==j and not truth[i]:P.extend(f's{i}:{p}' for p in MODES[False][2])
                P.append(f'h{j}:{int(b)}:{i+1}')
            P.append(f'u{j+1}')
        P.append('d0')
        for j,c in enumerate(self.clauses):
            i=next(i for i,(cl,x) in enumerate(occurrences) if cl==j and truth[i]);P.extend(f's{i}:{p}' for p in MODES[True][2]);P.append(f'd{j+1}')
        return tuple(P),tuple(Q)