From 4b8f598dea7980bf6a233ba2be2b87d8195d4940 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 15 Mar 2024 12:13:32 +0100 Subject: [PATCH] Sudoku's oplossen --- sudoku-v1.py | 107 +++++++++++++++++++++++++++++++++++++++++++++++++++ sudoku-v2.py | 101 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 208 insertions(+) create mode 100644 sudoku-v1.py create mode 100644 sudoku-v2.py diff --git a/sudoku-v1.py b/sudoku-v1.py new file mode 100644 index 0000000..b89ed3a --- /dev/null +++ b/sudoku-v1.py @@ -0,0 +1,107 @@ +# (Dit was de orginele versie die ik maakte voor een kennisclip bij de OU.) +# Voor dit python programm moet je een python pakket installeren. De wegpagine +# is https://pysathq.github.io. Je kunt dit pakker installeren met pip. +# Voer hiervoor het volgende commando uit in een terminal: +# +# pip install python-sat +# +# Daarna kun je het programma gebruiken: +# +# python3 sudoku-v1.py +# + +from pysat.solvers import Glucose3 + +next_var = 1 +var_dict = {} + +# x_r,c,d -> x_i +def var(r, c, d): + global next_var, var_dict + var_name = (r, c, d) + if var_name not in var_dict: + var_dict[var_name] = next_var + next_var = next_var + 1 + return var_dict[var_name] + +solver = Glucose3() + +def unique(lits): + solver.add_clause(lits) + for (i, l1) in enumerate(lits): + for l2 in lits[i+1:]: + solver.add_clause([-l1, -l2]) + + +# ********** +# SPELREGELS +# ********** + +# 0: in elk hokje precies 1 cijfer +for row in range(9): + for column in range(9): + unique([var(row, column, digit) for digit in range(1, 10)]) + +# 1. in elke rij staat elk cijfer precies 1 keer +for row in range(9): + for digit in range(1, 10): + unique([var(row, column, digit) for column in range(9)]) + +# 2. in elke kolom staat elk cijfer precies 1 keer +for column in range(9): + for digit in range(1, 10): + unique([var(row, column, digit) for row in range(9)]) + +# 3. in elk blok staat elk cijfer precies 1 keer +block_ranges = [range(0,3), range(3,6), range(6,9)] + +for row_block in block_ranges: + for column_block in block_ranges: + for digit in range(1, 10): + unique([var(row, column, digit) for row in row_block for column in column_block]) + + +# **************** +# GEGEVEN GETALLEN +# **************** + +# De drietallen staan voor (rij, kolom, getal) +known = [(0,3,7), (1,0,1), (2,3,4), (2,4,3), (2,6,2), + (3,8,6), (4,3,5), (4,5,9), (5,6,4), (5,7,1), (5,8,8), + (6,4,8), (6,5,1), (7,2,2), (7,7,5), (8,1,4), (8,6,3) + ] + +for (r, c, d) in known: + solver.add_clause([var(r, c, d)]) + + +# ******** +# OPLOSSEN +# ******** + + +num_sols = 0 +for m in solver.enum_models(): + model = {} + for l in m: + if l < 0: + model[-l] = False + else: + model[l] = True + + for row in range(9): + if row % 3 == 0: + print("") + for column in range(9): + if column % 3 == 0: + print(" ", end="") + for digit in range(1, 10): + if model[var(row, column, digit)]: + print(digit, end="") + print("") + print("") + + num_sols = num_sols + 1 + +print("Aantal oplossingen:") +print(num_sols) diff --git a/sudoku-v2.py b/sudoku-v2.py new file mode 100644 index 0000000..93af390 --- /dev/null +++ b/sudoku-v2.py @@ -0,0 +1,101 @@ +# Voor dit python programm moet je een python pakket installeren. De wegpagine +# is https://pysathq.github.io. Je kunt dit pakker installeren met pip. +# Voer hiervoor het volgende commando uit in een terminal: +# +# pip install python-sat +# +# Daarna kun je het programma gebruiken: +# +# python3 sudoku-v1.py +# + +# We importeren de SAT solver +from pysat.solvers import Solver +from pysat.formula import IDPool + +# Variabelen in pysat zijn altijd gegeven door een enkel getal. Maar wij hebben +# een variabele voor elke rij, kolom en cijfer. Met de "IDPool" kunnen we +# automatisch een drietal (rij, kolom, cijfer) laten vervangen door een enkel +# getal. +vpool = IDPool() +def var(r, c, d): + return(vpool.id((r, c, d))) + +# We maken een object om formules mee op te lossen. +solver = Solver() + +# Deze functie krijgt een lijst variabelen en voegt eisen toe aan de solver: +# 1. tenminste een van de variabelen moet waar zijn, en +# 2. tenhoogste een van de variabelen moet waar zijn. +# (Conclusie: precies 1 variabele moet waar zijn.) +def unique(lits): + solver.add_clause(lits) + for (i, l1) in enumerate(lits): + for l2 in lits[i+1:]: + solver.add_clause([-l1, -l2]) + + +# ********** +# SPELREGELS +# ********** + +# 0: in elk hokje precies 1 cijfer. +for row in range(9): + for column in range(9): + unique([var(row, column, digit) for digit in range(1, 10)]) + +# 1. in elke rij staat elk cijfer precies 1 keer. +for row in range(9): + for digit in range(1, 10): + unique([var(row, column, digit) for column in range(9)]) + +# 2. in elke kolom staat elk cijfer precies 1 keer. +for column in range(9): + for digit in range(1, 10): + unique([var(row, column, digit) for row in range(9)]) + +# 3. in elk blok staat elk cijfer precies 1 keer. +block_ranges = [range(0,3), range(3,6), range(6,9)] + +for row_block in block_ranges: + for column_block in block_ranges: + for digit in range(1, 10): + unique([var(row, column, digit) for row in row_block for column in column_block]) + +# Variaties (zoals de diagonaal) kunnen hier nog extra worden toegevoegd. + + +# **************** +# GEGEVEN GETALLEN +# **************** + +# De drietallen staan voor (rij, kolom, getal) +# Rijen en kolommen beginnen bij 0. +known = [(0,3,7), (1,0,1), (2,3,4), (2,4,3), (2,6,2), + (3,8,6), (4,3,5), (4,5,9), (5,6,4), (5,7,1), (5,8,8), + (6,4,8), (6,5,1), (7,2,2), (7,7,5), (8,1,4), (8,6,3) + ] + +# Voeg de gegeven getallen als formules toe aan de solver. +for (r, c, d) in known: + solver.add_clause([var(r, c, d)]) + + +# ******** +# OPLOSSEN +# ******** + +sat = solver.solve() + +# Als de solver het niet kan oplossen is er geen oplossing. +if not sat: + print('Er bestaat geen oplossing voor deze puzzel') + +# Anders is er wel een oplossing en die gaan we op het scherm tonen. +oplossing = solver.get_model() +for row in range(9): + for column in range(9): + for digit in range(1, 10): + if var(row, column, digit) in oplossing: + print(digit, end="") + print("")