In [ ]:

    

from pyeda.inter import *


    

In [ ]:

    

X = exprvars('x', 8, 8)


    

In [ ]:

    

R = And(*[OneHot(*[X[r,c] for c in range(8)]) for r in range(8)])


    

In [ ]:

    

C = And(*[OneHot(*[X[r,c] for r in range(8)]) for c in range(8)])


    

In [ ]:

    

starts = [(i, 0) for i in range(8-2, 0, -1)] + [(0, i) for i in range(8-1)]
lrdiags = []
for r, c in starts:
    lrdiags.append([])
    ri, ci = r, c
    while ri < 8 and ci < 8:
        lrdiags[-1].append((ri, ci))
        ri += 1
        ci += 1

DLR = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in lrdiags])


    

In [ ]:

    

starts = [(i, 8-1) for i in range(8-2, -1, -1)] + [(0, i) for i in range(8-2, 0, -1)]
rldiags = []
for r, c in starts:
    rldiags.append([])
    ri, ci = r, c
    while ri < 8 and ci >= 0:
        rldiags[-1].append((ri, ci))
        ri += 1
        ci -= 1

DRL = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in rldiags])


    

In [ ]:

    

S = And(R, C, DLR, DRL)


    

In [ ]:

    

S.is_cnf()


    

In [ ]:

    

len(S.xs)


    

In [ ]:

    

def display(point):
    chars = list()
    for r in range(8):
        for c in range(8):
            if point[X[r,c]]:
                chars.append("Q")
            else:
                chars.append(".")
        if r != 7:
            chars.append("\n")
    print("".join(chars))


    

In [ ]:

    

display(S.satisfy_one())


    

In [ ]:

    

for i, soln in enumerate(S.satisfy_all()):
    print("Solution", i+1, end="\n\n")
    display(soln)
    print("")


    

In [ ]:

    

S.satisfy_count()


    

In [ ]:

    

len(list(S.satisfy_all()))


    

In [ ]: