-
Notifications
You must be signed in to change notification settings - Fork 5
/
starbattle.py
60 lines (46 loc) · 1.51 KB
/
starbattle.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
from collections import defaultdict
from grid import Grid
import z3
import display
givens = [
"aaabbbbccd",
"aaabccbccd",
"aaabcccccd",
"aaaacceedd",
"ffeeeeeedd",
"ffffeggggd",
"ffhffggggd",
"iihhgggggd",
"ijjhhhhggd",
"ijjjjhgggg",
]
board = Grid(len(givens[0]), len(givens), "grid", cellgen=z3.Int)
s = z3.Solver()
for cell in board.cells:
s.add(cell.var >= 0)
s.add(cell.var <= 1)
# build regions
regions = defaultdict(list)
for y, row in enumerate(givens):
for x, cell in enumerate(row):
regions[cell].append(board.cell(x, y).var)
for region in regions.values():
s.add(z3.Sum(region) == 2)
for y in range(board.height):
s.add(z3.Sum([board.cell(x, y).var for x in range(board.width)]) == 2)
for x in range(board.width):
s.add(z3.Sum([board.cell(x, y).var for y in range(board.height)]) == 2)
for e in board.edges:
s.add(z3.Sum([cell.var for cell in e.cells()]) < 2)
for p in board.points:
if p.is_outside: continue
s.add(z3.Sum(p.edge_left.cell_above.var, p.edge_right.cell_below.var) < 2)
s.add(z3.Sum(p.edge_left.cell_below.var, p.edge_right.cell_above.var) < 2)
print(s.check())
m = s.model()
def draw_edge(ctx:display.EdgeContext):
ctx.draw(width=5 if (ctx.edge.is_outside or len({givens[cell.y][cell.x] for cell in ctx.edge.cells()}) == 2) else 1)
def draw_cell(ctx:display.CellContext):
if ctx.val == "1":
ctx.circle(fill=True)
display.draw_grid(board, m, 64, cell_fn=draw_cell, vert_fn=draw_edge, horiz_fn=draw_edge)