Sudoku's oplossen

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)

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("")