1
Fork 0
mirror of https://git.cs.ou.nl/joshua.moerman/puzzels.git synced 2025-05-14 00:37:45 +02:00

puzzeltje

This commit is contained in:
Joshua Moerman 2025-01-29 10:29:53 +01:00
parent b36d09102d
commit f42d619b12

108
clowns.py Normal file
View file

@ -0,0 +1,108 @@
from pysat.solvers import Solver
from pysat.formula import IDPool
from pysat.card import CardEnc, EncType
tegels = {
1: 'roypgb',
2: 'rybopg',
3: 'rogybp',
4: 'rbpgoy',
5: 'rgpbyo',
6: 'robpyg',
7: 'rpoybg',
}
plaatsen = 'ABCDEFG'
richtingen = [0, 1, 2, 3, 4, 5]
paren = [
(('C', 0), ('A', 3)),
(('C', 1), ('D', 4)),
(('C', 2), ('G', 5)),
(('C', 3), ('F', 0)),
(('C', 4), ('E', 1)),
(('C', 5), ('B', 2)),
(('A', 2), ('D', 5)),
(('D', 3), ('G', 0)),
(('G', 4), ('F', 1)),
(('F', 5), ('E', 2)),
(('E', 0), ('B', 3)),
(('B', 1), ('A', 4)),
]
assert len(tegels) == 7
assert len(set(tegels.keys())) == 7
assert len(set(tegels.values())) == 7
assert len(plaatsen) == 7
assert len(set(plaatsen)) == 7
assert len(paren) == 12
for (p1, r1), (p2, r2) in paren:
assert p1 != p2
assert 0 <= r1 and r1 < 6 and 0 <= r2 and r2 < 6
assert (r2 - r1) % 6 == 3
vpool = IDPool()
solver = Solver()
def var_tegel(tegel, plaats, richting):
assert tegel in tegels
assert plaats in plaatsen
assert 0 <= richting and richting < 6
return vpool.id((tegel, plaats, richting))
def unique(lits):
cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.pairwise)
solver.append_formula(cnf.clauses)
for tegel in tegels:
unique([var_tegel(tegel, p, r) for p in plaatsen for r in richtingen])
# solver.solve()
# print(solver.get_model())
# solver.solve()
# m = solver.get_model()
# for lit in m:
# if lit < 0:
# print(f'{vpool.id2obj[-lit]} is onwaar')
# else:
# print(f'{vpool.id2obj[lit]} is waar')
for plaats in plaatsen:
unique([var_tegel(t, plaats, r) for t in tegels for r in richtingen])
# solver.solve()
# m = solver.get_model()
# for lit in m:
# if lit > 0:
# print(f'{vpool.id2obj[lit]} is waar')
for (p1, r1), (p2, r2) in paren:
for t1 in tegels:
for t2 in tegels:
for d1 in richtingen:
for d2 in richtingen:
if tegels[t1][(r1 - d1) % 6] != tegels[t2][(r2 - d2) % 6]:
solver.add_clause([-var_tegel(t1, p1, d1), -var_tegel(t2, p2, d2)])
# solver.solve()
# m = solver.get_model()
# for lit in m:
# if lit > 0:
# print(f'{vpool.id2obj[lit]} is waar')
oplossingen = 0
while solver.solve():
m = solver.get_model()
solver.add_clause([-lit for lit in m])
oplossingen += 1
print(oplossingen)