puzzels/sudoku-v1.py

# (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 pakket 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)