# This program finds shortest paths of length 6 from [1,2,3,4,5] to [6,7,8,9,10] # with all possible outmaps for [1,2,3,4,5] sixpathsx=[[[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[8,7,3,4,5],[8,7,9,4,5],[8,7,9,6,5],[8,7,9,6,10]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[8,7,3,4,5],[8,7,9,4,5],[8,7,9,10,5],[8,7,9,10,6]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[9,7,8,4,5],[9,7,8,10,5],[9,7,8,10,6]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[6,9,8,4,5],[6,9,8,10,5],[6,9,8,10,7]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,8,5],[6,7,9,8,5],[6,7,9,8,10]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,8,5],[6,7,1,8,9],[6,7,10,8,9]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[6,7,8,1,5],[6,7,8,1,9],[6,7,8,10,9]], [[1,2,3,4,5],[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[6,7,8,2,5],[6,7,8,2,9],[6,7,8,10,9]]] def listsigma(os1): #this function computes the parity of a list sig=1 for i in range(1,len(os1)): for j in range(i): if os1[j]>os1[i]: sig=-sig return sig pathlist=sixpathsx d=len(pathlist[0][0]) n=2*d for mp in range(len(pathlist)): print(pathlist[mp]) outmaps=Subsets([2,3,4,5]) outlist=outmaps.list() for v in range(len(outmaps)): solver=SAT() S=Subsets(n+2,d+1) solver.add_clause((1,2)) #make chi(1,2,...,d+1) equal to one solver.add_clause((1,-2)) nlistzero=[j for j in [1..d]] s2=S.rank(nlistzero+[n+2])+1 for i in range(4): if i+1 in outlist[v]: nlistzerof=nlistzero[:] nlistzerof[i+1]=n+1 solver.add_clause((listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),-s2)) solver.add_clause((-listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),s2)) if i+1 not in outlist[v]: nlistzerof=nlistzero[:] nlistzerof[i+1]=n+1 solver.add_clause((-listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),-s2)) solver.add_clause((listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),s2)) print(outmaps[v]) nlistzero=[j for j in [1..d]] #make 1,2,...,d a vertex for i in [d+1..n]: s1=S.rank(nlistzero+[i])+1 s2=S.rank(nlistzero+[n+2])+1 solver.add_clause((s1,-s2)) solver.add_clause((-s1,s2)) nlistzerof=nlistzero[:] nlistzerof[0]=n+1 solver.add_clause((listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),-s2)) solver.add_clause((-listsigma(nlistzerof+[n+2])*(S.rank(nlistzerof+[n+2])+1),s2)) for k in range(len(pathlist[mp])-1): #Go through the vertices of the path pathlist[m] nlistk=pathlist[mp][k] nlistkpone=pathlist[mp][k+1] s2=listsigma(nlistk+[n+2])*(S.rank(nlistk+[n+2])+1) #make pathlist[m][k] a vertex for i in [1..2*d]: if i not in nlistk: s1=listsigma(nlistk+[i])*(S.rank(nlistk+[i])+1) solver.add_clause((s1,-s2)) solver.add_clause((-s1,s2)) for i in [1..d]: if nlistk[i-1] not in nlistkpone: #orient the edge leaving pathlist[m][k] nlistkf=nlistk[:] nlistkf[i-1]=n+1 s1=listsigma(nlistkf+[n+2])*(S.rank(nlistkf+[n+2])+1) solver.add_clause((s1,-s2)) solver.add_clause((-s1,s2)) nlistd=[j for j in [d+1..n]] #make d+1,..,2d a vertex for i in [1..d]: solver.add_clause((S.rank([i]+nlistd)+1,((-1)^d)*(-(S.rank(nlistd+[n+2])+1)))) solver.add_clause((-(S.rank([i]+nlistd)+1),((-1)^d)*((S.rank(nlistd+[n+2])+1)))) for i in [1..d]: #make d+1,..,2d the sink. nlistdi=nlistd[:] nlistdi[i-1]=n+1 solver.add_clause((S.rank(nlistd+[n+2])+1,((-1)^(d-i))*(S.rank(nlistdi+[n+2])+1))) solver.add_clause((-(S.rank(nlistd+[n+2])+1),-((-1)^(d-i))*(S.rank(nlistdi+[n+2])+1))) grset=Set(range(1,n+3)) #This block gives the chirotope clauses. T=Subsets(n+2,d-1) for i in range(len(T)): tau=sorted(T[i]) taubar=grset.difference(T[i]) taubars=sorted(taubar) Ti=Subsets(taubars,4) for j in range(len(Ti)): rho=sorted(Ti[j]) alpha=tau+[rho[0],rho[1]] signa=1 for k in range(d-1): if tau[k]>rho[0]: signa=-signa if tau[k]>rho[1]: signa=-signa sa=S.rank(alpha)+1 beta=tau+[rho[2],rho[3]] signb=1 for k in range(d-1): if tau[k]>rho[2]: signb=-signb if tau[k]>rho[3]: signb=-signb sb=S.rank(beta)+1 gamma=tau+[rho[0],rho[2]] signc=1 for k in range(d-1): if tau[k]>rho[0]: signc=-signc if tau[k]>rho[2]: signc=-signc sc=S.rank(gamma)+1 delta=tau+[rho[1],rho[3]] signd=1 for k in range(d-1): if tau[k]>rho[1]: signd=-signd if tau[k]>rho[3]: signd=-signd sd=S.rank(delta)+1 epsi=tau+[rho[0],rho[3]] signe=1 for k in range(d-1): if tau[k]>rho[0]: signe=-signe if tau[k]>rho[3]: signe=-signe se=S.rank(epsi)+1 phi=tau+[rho[1],rho[2]] signf=1 for k in range(d-1): if tau[k]>rho[1]: signf=-signf if tau[k]>rho[2]: signf=-signf sf=S.rank(phi)+1 solver.add_clause((-signa*sa,-signb*sb,-signc*sc,signd*sd,-signe*se,-signf*sf)) solver.add_clause((-signa*sa,-signb*sb,-signc*sc,signd*sd,signe*se,signf*sf)) solver.add_clause((-signa*sa,-signb*sb,signc*sc,-signd*sd,-signe*se,-signf*sf)) solver.add_clause((-signa*sa,-signb*sb,signc*sc,-signd*sd,signe*se,signf*sf)) solver.add_clause((-signa*sa,signb*sb,-signc*sc,-signd*sd,-signe*se,signf*sf)) solver.add_clause((-signa*sa,signb*sb,-signc*sc,-signd*sd,signe*se,-signf*sf)) solver.add_clause((-signa*sa,signb*sb,signc*sc,signd*sd,-signe*se,signf*sf)) solver.add_clause((-signa*sa,signb*sb,signc*sc,signd*sd,signe*se,-signf*sf)) solver.add_clause((signa*sa,-signb*sb,-signc*sc,-signd*sd,-signe*se,signf*sf)) solver.add_clause((signa*sa,-signb*sb,-signc*sc,-signd*sd,signe*se,-signf*sf)) solver.add_clause((signa*sa,-signb*sb,signc*sc,signd*sd,-signe*se,signf*sf)) solver.add_clause((signa*sa,-signb*sb,signc*sc,signd*sd,signe*se,-signf*sf)) solver.add_clause((signa*sa,signb*sb,-signc*sc,signd*sd,-signe*se,-signf*sf)) solver.add_clause((signa*sa,signb*sb,-signc*sc,signd*sd,signe*se,signf*sf)) solver.add_clause((signa*sa,signb*sb,signc*sc,-signd*sd,-signe*se,-signf*sf)) solver.add_clause((signa*sa,signb*sb,signc*sc,-signd*sd,signe*se,signf*sf)) p=Permutations(d) #This block eliminates directed paths of length 5. q=Permutations(d) for i in range(len(p)): for j in range(len(p)): newlits=[] sigi=1 nb=[m for m in [1..d]] nbg=[m for m in [1..d]]+[2*d+2] for k in range(d+1): if k > 0: nb[p[i][k-1]-1]=q[j][k-1]+d sigi=-sigi nbg[p[i][k-1]-1]=q[j][k-1]+d if k2*d+1: nbpl=nb+[l] nl=sigi*listsigma(nbpl)*(S.rank(nbpl)+1) newlits=newlits+[nl] if k==d: newlits=newlits+[sigi*listsigma(nbg)*(S.rank(nbg)+1)] newlitsneg=[-newlits[t] for t in range(len(newlits))] solver.add_clause(tuple(newlitsneg)) outp=solver() print(outp)