Lesson 8

And here is how with the help of the \(\texttt{PySAT}\) module you can solve the sixteen diagonals puzzle. In the code below we create a Boolean variable for each diagonal. Then, for any two intersecting diagonals (we check this using the \(\texttt{shapely}\) module) we create a 2-clause explicitly forbidding these two diagonals simultaneously. Finally, using the \(\texttt{atleast}\) method we require that there are at least sixteen diagonals.

from itertools import combinations, product
from pysat.solvers import Solver
from pysat.card import *
from pysat.formula import IDPool, CNF
from shapely.geometry import LineString


n, num_diagonals = 5, 16

segments = {}
pool, formula = IDPool(), CNF()

for x, y in product(range(n + 1), repeat=2):
    for a, b in product((-1, 1), repeat=2):
        if x + a in range(n + 1) and y + b in range(n + 1):
            segments[x, y, x + a, y + b] = pool.id((x, y, x + a, y + b))

for s1, s2 in combinations(segments, 2):
    if LineString([s1[:2], s1[2:]]).intersects(LineString([s2[:2], s2[2:]])):
        formula.append([-segments[s1], -segments[s2]])

formula.extend(CardEnc.atleast(lits=segments.values(), bound=num_diagonals, vpool=pool))

solver = Solver(bootstrap_with=formula)
solver.solve()
model = solver.get_model()

for s in segments:
    if segments[s] in model:
        print(s)

(1, 0, 0, 1)
(1, 2, 2, 3)
(1, 3, 0, 2)
(1, 4, 0, 3)
(1, 5, 0, 4)
(2, 0, 1, 1)
(2, 1, 3, 0)
(3, 1, 2, 2)
(3, 2, 4, 3)
(3, 3, 2, 4)
(3, 4, 2, 5)
(4, 0, 5, 1)
(4, 4, 3, 5)
(5, 2, 4, 1)
(5, 3, 4, 2)
(5, 4, 4, 5)