#This is a sage program that shows Delta_{sm}(5,10)=5.

#this function determines the parity of a permutation.
def listsigma(os1):
    sig=1
    for i in range(1,len(os1)):
        for j in range(i):
            if os1[j]>os1[i]:
                sig=-sig
    return sig

#These are the eight monotone paths that will be forced in different runs of the program.
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]]]

#After Delta_{sm}(5,10)=5 has been verified for acyclic orientations by showing no examples 
#with strict monotone diameter 6 exist, one can search for orientations containing cycles 
#and strict monotone diameter 7 by replacing sixpathsx by sevenpathsonerev in pathlist.
sevenpathsonerev=[[[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[6,7,8,1,5],[6,7,8,1,2],[6,7,8,9,2],[6,7,8,9,10]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,8,4,5],[6,7,8,2,5],[6,7,8,2,1],[6,7,8,9,1],[6,7,8,9,10]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,8,5],[6,7,1,8,2],[6,7,9,8,2],[6,7,9,8,10]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,8,5],[6,7,2,8,5],[6,7,2,8,9],[6,7,10,8,9]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,2,5],[6,7,1,2,8],[6,7,9,2,8],[6,7,9,10,8]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,2,5],[6,7,8,2,5],[6,7,8,2,9],[6,7,8,10,9]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,2,5],[6,7,1,2,8],[6,7,1,9,8],[6,7,10,9,8]],
[[6,2,3,4,5],[6,7,3,4,5],[6,7,1,4,5],[6,7,1,2,5],[6,7,8,2,5],[6,7,8,9,5],[6,7,8,9,10]]]

pathlist=sixpathsx

for m in range(len(pathlist)):
    solver=SAT()

    d=len(pathlist[0][0])
    n=2*d
    S=Subsets(n+2,d+1)
    solver.add_clause((1,2))# This forces chi([1,2,3,4,5]) to be +1.
    solver.add_clause((1,-2))

    nlistzero=[j for j in [1..d]]#These lines make [1,2,3,4,5] 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))
        print(nlistzero+[i],nlistzero+[n+2])
    for i in [1..d]:#These lines orient the arcs away from [1,2,3,4,5]
        nlistzeroi=nlistzero[:]
        nlistzeroi[i-1]=n+1
        solver.add_clause((S.rank(nlistzero+[n+2])+1,-((-1)^(d-i))*(S.rank(nlistzeroi+[n+2])+1)))
        solver.add_clause((-(S.rank(nlistzero+[n+2])+1),((-1)^(d-i))*(S.rank(nlistzeroi+[n+2])+1)))
        print(nlistzero+[n+2],((-1)^(d-i)),nlistzeroi+[n+2])

    for k in range(len(pathlist[m])-1):
        nlistk=pathlist[m][k]
        nlistkpone=pathlist[m][k+1]
        s2=listsigma(nlistk+[n+2])*(S.rank(nlistk+[n+2])+1)
        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))
                print(nlistk+[i],nlistk+[n+2])
        for i in [1..d]:
            if nlistk[i-1] not in nlistkpone:
                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))
                print(nlistkf+[n+2],nlistk+[n+2])

    nlistd=[j for j in [d+1..n]]
    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))))
        print([i]+nlistd,((-1)^d),nlistd+[n+2])
    for i in [1..d]:
        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)))
        print(nlistd+[n+2],-((-1)^(d-i)),nlistdi+[n+2])

    grset=Set(range(1,n+3))
    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)
    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 k<d:
                        nbfgl=nbg[:]
                        nbfge=nbg[:]
                        nbfgl[p[i][k]-1]=2*d+1
                        nbfge[p[i][k-1]-1]=2*d+1
                        newlits=newlits+[sigi*listsigma(nbfgl)*(S.rank(nbfgl)+1)]
                        newlits=newlits+[sigi*-listsigma(nbfge)*(S.rank(nbfge)+1)]
                        for l in [1..2*d+2]:
                            if l not in nb and l<>2*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))
    solver()