# 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-v2.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("")