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