v3 die ook grotere sudokus kan oplossen en input kan lezen

sudoku-v3.py

@@ -0,0 +1,121 @@
+# Veranderingen t.o.v. v1 en v2:
+# * Ik maak nu gebruik van CardEnc om formules te maken (ipv met de hand)
+# * Het script kan sudokus inlezen (alleen voor 4x4, 9x9 en FxF (hexadecimaal))
+# * Het script kan ook grotere sudokus oplossen
+
+from pysat.solvers import Solver
+from pysat.formula import IDPool
+from pysat.card import CardEnc, EncType
+
+# Dit is voor een 9x9 bord
+small_size = 3
+full_size = small_size*small_size
+
+
+# *******
+# PARSING
+# *******
+
+def is_nonzero_digit(c):
+  return ('1' <= c and c <= '9') or ('a' <= c and c <= 'f')
+
+# sudocue.net format
+def read_input():
+  givens = []
+  line = input()
+  chunks = [line[i:i+full_size] for i in range(0, full_size*full_size, full_size)]
+  for row in range(full_size):
+    for column in range(full_size):
+      c = chunks[row][column]
+      if is_nonzero_digit(c):
+        givens.append((row, column, int(c, base=16)))
+  return givens
+
+known = read_input()
+
+
+# ************
+# SOLVER SETUP
+# ************
+
+vpool = IDPool()
+solver = Solver()
+
+# mapping van variabeles: x_{r,c,d}  ->  x_i
+def var(r, c, d):
+  return(vpool.id(("sudoku", r, c, d)))
+
+# maakt de constraint dat precies een van de literals waar moet zijn
+def unique(lits):
+  # deze werken goed: pairwise, seqcounter, bitwise, mtotalizer, kmtotalizer
+  # anderen geven groter aantal oplossingen
+  # alles behalve pairwise introduceert meer variabelen
+  cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
+  solver.append_formula(cnf.clauses)
+
+
+# **********
+# SPELREGELS
+# **********
+
+# 0: in elk hokje precies 1 cijfer
+for row in range(full_size):
+  for column in range(full_size):
+    unique([var(row, column, digit) for digit in range(1, full_size+1)])
+
+# 1. in elke rij staat elk cijfer precies 1 keer
+for row in range(full_size):
+  for digit in range(1, full_size+1):
+    unique([var(row, column, digit) for column in range(full_size)])
+
+# 2. in elke kolom staat elk cijfer precies 1 keer
+for column in range(full_size):
+  for digit in range(1, full_size+1):
+    unique([var(row, column, digit) for row in range(full_size)])
+
+# 3. in elk blok staat elk cijfer precies 1 keer
+block_ranges = [range(i, i+small_size) for i in range(0, full_size, small_size)]
+
+for row_block in block_ranges:
+  for column_block in block_ranges:
+    for digit in range(1, full_size+1):
+      unique([var(row, column, digit) for row in row_block for column in column_block])
+
+
+# ****************
+# GEGEVEN GETALLEN
+# ****************
+
+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(full_size):
+    if row % small_size == 0:
+      print("")
+    for column in range(full_size):
+      if column % small_size == 0:
+        print(" ", end="")
+      for digit in range(1, full_size+1):
+        if model[var(row, column, digit)]:
+          print(digit, end="")
+    print("")
+  print("")
+
+  num_sols = num_sols + 1
+
+print("Aantal oplossingen:")
+print(num_sols)