mirror of
https://git.cs.ou.nl/joshua.moerman/puzzels.git
synced 2025-05-13 16:27:44 +02:00
101 lines
2.9 KiB
Python
101 lines
2.9 KiB
Python
# 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("")
|