diff --git a/sudoku-v3.py b/sudoku-v3.py new file mode 100644 index 0000000..c88e3e6 --- /dev/null +++ b/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)