from pysat.solvers import Solver
from pysat.formula import CNF

# Encode Sudoku as CNF
def sudoku_to_sat(grid):
    cnf = CNF()

    def varnum(r, c, d):
        return 81 * (r - 1) + 9 * (c - 1) + d

    # 1. At least one digit per cell
    for r in range(1, 10):
        for c in range(1, 10):
            cnf.append([varnum(r, c, d) for d in range(1, 10)])

    # 2. No two digits in the same cell
    for r in range(1, 10):
        for c in range(1, 10):
            for d1 in range(1, 10):
                for d2 in range(d1 + 1, 10):
                    cnf.append([-varnum(r, c, d1), -varnum(r, c, d2)])

    # 3. Row constraints
    for r in range(1, 10):
        for d in range(1, 10):
            for c1 in range(1, 10):
                for c2 in range(c1 + 1, 10):
                    cnf.append([-varnum(r, c1, d), -varnum(r, c2, d)])

    # 4. Column constraints
    for c in range(1, 10):
        for d in range(1, 10):
            for r1 in range(1, 10):
                for r2 in range(r1 + 1, 10):
                    cnf.append([-varnum(r1, c, d), -varnum(r2, c, d)])

    # 5. Subgrid constraints
    for br in range(0, 3):
        for bc in range(0, 3):
            for d in range(1, 10):
                cells = []
                for r in range(3 * br + 1, 3 * br + 4):
                    for c in range(3 * bc + 1, 3 * bc + 4):
                        cells.append((r, c))
                for i in range(len(cells)):
                    for j in range(i + 1, len(cells)):
                        r1, c1 = cells[i]
                        r2, c2 = cells[j]
                        cnf.append([-varnum(r1, c1, d), -varnum(r2, c2, d)])

    # 6. Pre-filled cells
    for r in range(1, 10):
        for c in range(1, 10):
            if grid[r - 1][c - 1] != 0:
                d = grid[r - 1][c - 1]
                cnf.append([varnum(r, c, d)])

    return cnf

# Solve Sudoku
def solve_sudoku(grid):
    cnf = sudoku_to_sat(grid)
    solver = Solver(name='glucose3')  # you can use 'cadical', 'minisat22', etc.
    solver.append_formula(cnf.clauses)

    if solver.solve():
        model = solver.get_model()
        solution = [[0 for _ in range(9)] for _ in range(9)]
        for v in model:
            if v > 0:
                v -= 1
                r = v // 81 + 1
                c = (v % 81) // 9 + 1
                d = (v % 9) + 1
                solution[r - 1][c - 1] = d
        solver.delete()
        return solution
    else:
        solver.delete()
        return None

# Example Sudoku (0 = blank)
grid = [
    [1, 0, 0, 0, 0, 0, 0, 8, 0],
    [6, 0, 0, 0, 0, 0, 5, 3, 0],
    [8, 0, 0, 0, 1, 7, 0, 0, 0],
    [0, 0, 2, 8, 0, 3, 0, 0, 5],
    [0, 0, 8, 0, 0, 4, 0, 0, 7],
    [0, 0, 0, 0, 0, 0, 0, 0, 9],
    [0, 4, 0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 9, 6, 0, 0, 5, 0],
    [0, 1, 0, 0, 2, 0, 6, 0, 0]
]

solution = solve_sudoku(grid)

if solution:
    for row in solution:
        print(row)
else:
    print("No solution found!")