puzzle-solvers

 1import sys
 2import time
 3
 4import z3
 5
 6
 7def solve(puzzle):
 8    s = z3.Solver()
 9
10    start = time.time()
11
12    vars = []
13    for i in range(0, 9**2):
14        x = i % 9
15        y = int(i / 9)
16
17        v = z3.Int(f"{x},{y}")
18        n = int(puzzle[i])
19        if n == 0:
20            s.add(v >= 1, v <= 9)
21        else:
22            s.add(v == n)
23
24        vars.append(v)
25
26    # rows
27    for y in range(9):
28        for x1 in range(9):
29            for x2 in range(9):
30                if x1 == x2:
31                    continue
32                s.add(vars[y * 9 + x1] != vars[y * 9 + x2])
33
34    # cols
35    for x in range(9):
36        for y1 in range(9):
37            for y2 in range(9):
38                if y1 == y2:
39                    continue
40                s.add(vars[y1 * 9 + x] != vars[y2 * 9 + x])
41
42    # boxes
43    for yi in range(0, 3):
44        for xi in range(0, 3):
45            y_top = yi * 3
46            x_top = xi * 3
47
48            for y1 in range(y_top, y_top + 3):
49                for x1 in range(x_top, x_top + 3):
50                    for y2 in range(y_top, y_top + 3):
51                        for x2 in range(x_top, x_top + 3):
52                            if y1 == y2 and x1 == x2:
53                                continue
54                            s.add(vars[y1 * 9 + x1] != vars[y2 * 9 + x2])
55
56    done_constructing = time.time()
57
58    if s.check() == z3.sat:
59        model = s.model()
60        for y in range(0, 9):
61            for x in range(0, 9):
62                print("{}".format(model[vars[y * 9 + x]]), end="")
63            print()
64        print()
65    else:
66        print("AAAH")
67
68    done = time.time()
69
70    print(
71        "time spent constructing: {}\ntime spent solving: {}\ntotal: {}".format(
72            done_constructing - start, done - done_constructing, done - start
73        )
74    )
75
76
77puzzles = []
78with open(sys.argv[1]) as f:
79    for line in f:
80        line = line.strip().replace(".", "0")
81        assert len(line) == 81
82        solve(line)