from pysat.solvers import Solver


def n_queens(n: int) -> None:
    # 1 2 3
    # 4 5 6
    # 7 8 9
    def b(r, c):
        return n * (r - 1) + c

    def sweep(sr: int, sc: int, dr: int, dc: int) -> list[int]:
        assert 1 <= sr <= n and 1 <= sc <= n

        r = sr
        c = sc
        res = []

        while 1 <= r <= n and 1 <= c <= n:
            res.append(b(r, c))
            r += dr
            c += dc

        return res

    def row(r: int) -> list[int]:
        return sweep(r, 1, 0, 1)

    def col(c: int) -> list[int]:
        return sweep(1, c, 1, 0)

    def diagonal(r: int, c: int) -> list[int]:
        return sweep(r, c, 1, 1)

    def antidiagonal(r: int, c: int) -> list[int]:
        return sweep(r, c, 1, -1)

    def at_least_one(literals: list[int]) -> list[list[int]]:
        return [literals]

    def at_most_one(literals: list[int]) -> list[list[int]]:
        cnf = []

        for i in range(len(literals) - 1):
            for j in range(i + 1, len(literals)):
                cnf.append([-literals[i], -literals[j]])

        return cnf

    def exactly_one(literals: list[int]) -> list[list[int]]:
        return at_most_one(literals) + at_least_one(literals)

    def print_solution(model: list[int]) -> None:
        for r in range(1, n + 1):
            for c in range(1, n + 1):
                if b(r, c) in model:
                    print('Q', end=' ')
                else:
                    print('.', end=' ')
            print()

    with Solver() as s:
        for r in range(1, n + 1):
            s.append_formula(exactly_one(row(r)))

        for c in range(1, n + 1):
            s.append_formula(exactly_one(col(c)))

        for r in range(1, n):
            s.append_formula(at_most_one(diagonal(r, 1)))

        for c in range(2, n):
            s.append_formula(at_most_one(diagonal(1, c)))

        for r in range(1, n):
            s.append_formula(at_most_one(antidiagonal(r, n)))

        for c in range(2, n):
            s.append_formula(at_most_one(antidiagonal(1, c)))

        sat = s.solve()

        if not sat:
            print('For n =', n, 'there is no solution.')
        else:
            print_solution(s.get_model())


n_queens(8)