puzzels/sudoku-v3.py

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