Skip to content

Instantly share code, notes, and snippets.

@Addelec

Addelec/Solution.ipynb Secret

Created November 28, 2025 11:23
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save Addelec/5a6c60c0b2295dc9a2ae913ea3c469f6 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save Addelec/5a6c60c0b2295dc9a2ae913ea3c469f6 to your computer and use it in GitHub Desktop.
Download ZIP
Shut the Box - Solution
Display the source blob
Display the rendered blob
Raw
Solution.ipynb
{
"cells": [
{
"cell_type": "code",
"execution_count": 12,
"id": "ccd35f00",
"metadata": {},
"outputs": [],
"source": [
"from enum import Enum\n",
"import pygame"
]
},
{
"cell_type": "code",
"execution_count": 13,
"id": "51e8f9e1",
"metadata": {},
"outputs": [],
"source": [
"CellState = Enum('CellState', 'UNSURE OUTSIDE INSIDE POSSIBLE ARROW', start=0)\n",
"ARROW_DIRECTIONS = Enum('ARROW_DIRECTIONS', 'NORTH SOUTH EAST WEST', start=0)\n",
"\n",
"class GridCell:\n",
" def __init__(self, x, y):\n",
" self.x = x\n",
" self.y = y\n",
" self.value = 0\n",
" self.state = CellState.UNSURE\n",
" self.highlighted = False\n",
" self.arrow_directions = set() # Set of directions in which arrows are present\n",
" self.state_locked = False\n",
" \n",
" def get_cardinal_neighbours(self, grid):\n",
" directions = {\n",
" 'NORTH': (-1, 0),\n",
" 'SOUTH': (1, 0),\n",
" 'EAST': (0, 1),\n",
" 'WEST': (0, -1),\n",
" }\n",
" neighbours = {}\n",
" for dir_name, (dy, dx) in directions.items():\n",
" ny, nx = self.y + dy, self.x + dx\n",
" if 0 <= ny < len(grid) and 0 <= nx < len(grid[0]):\n",
" neighbours[dir_name] = grid[ny][nx]\n",
" else:\n",
" neighbours[dir_name] = None\n",
" return neighbours\n",
" \n",
" def get_neighbourhood(self, grid):\n",
" neighbourhood = []\n",
" for dy in [-1, 0, 1]:\n",
" row = []\n",
" for dx in [-1, 0, 1]:\n",
" ny, nx = self.y + dy, self.x + dx\n",
" if 0 <= ny < len(grid) and 0 <= nx < len(grid[0]):\n",
" row.append(grid[ny][nx])\n",
" else:\n",
" row.append(None)\n",
" neighbourhood.append(row)\n",
" return neighbourhood"
]
},
{
"cell_type": "code",
"execution_count": 14,
"id": "4c36f933",
"metadata": {},
"outputs": [],
"source": [
"GRID_SIZE = 20\n",
"# Create grid of GridCells\n",
"grid = [[GridCell(x, y) for x in range(GRID_SIZE)] for y in range(GRID_SIZE)]"
]
},
{
"cell_type": "code",
"execution_count": 15,
"id": "b82dd972",
"metadata": {},
"outputs": [],
"source": [
"def check_if_outside_valid():\n",
" valid_set = set()\n",
" all_valid = True\n",
" for row in grid:\n",
" for cell in row:\n",
" if cell.state == CellState.OUTSIDE and cell not in valid_set:\n",
" # Floodfill to find connected outside cells (cardinal directions)\n",
" component = set()\n",
" queue = [cell]\n",
" visited = set()\n",
" while queue:\n",
" c = queue.pop(0)\n",
" if c in visited:\n",
" continue\n",
" visited.add(c)\n",
" component.add(c)\n",
" neighs = c.get_cardinal_neighbours(grid)\n",
" for n in neighs.values():\n",
" if n and n.state == CellState.OUTSIDE and n not in visited:\n",
" queue.append(n)\n",
" # Check if any cell in component is at the edge\n",
" at_edge = any(c.y == 0 or c.y == len(grid) - 1 or c.x == 0 or c.x == len(grid[0]) - 1 for c in component)\n",
" if not at_edge:\n",
" # Invalid: highlight all cells in component\n",
" for c in component:\n",
" c.highlighted = True\n",
" all_valid = False\n",
" else:\n",
" valid_set.update(component)\n",
" return all_valid\n",
"\n",
"def check_if_inside_valid():\n",
" inside_cells = [cell for row in grid for cell in row if cell.state == CellState.INSIDE]\n",
" if not inside_cells:\n",
" return True\n",
" # Floodfill from the first inside cell\n",
" visited = set()\n",
" queue = [inside_cells[0]]\n",
" while queue:\n",
" c = queue.pop(0)\n",
" if c in visited:\n",
" continue\n",
" visited.add(c)\n",
" neighs = c.get_cardinal_neighbours(grid)\n",
" for n in neighs.values():\n",
" if n and n.state == CellState.INSIDE and n not in visited:\n",
" queue.append(n)\n",
" # Check if all inside cells are connected\n",
" if len(visited) == len(inside_cells):\n",
" return True\n",
" else:\n",
" # Highlight disconnected inside cells\n",
" for c in inside_cells:\n",
" if c not in visited:\n",
" c.highlighted = True\n",
" return False\n",
"\n",
"def is_number_cell_valid(cell):\n",
" if cell.value == 0:\n",
" return True # 0 cells are always valid\n",
" \n",
" neighbourhood = cell.get_neighbourhood(grid)\n",
" inside_count = sum(1 for r in neighbourhood for c in r if c and c.state == CellState.INSIDE)\n",
" return inside_count == cell.value\n",
"\n",
"def is_arrow_cell_valid(cell):\n",
" if not cell.arrow_directions:\n",
" return True # Though probably not called without arrows\n",
" \n",
" directions = [ARROW_DIRECTIONS.NORTH, ARROW_DIRECTIONS.SOUTH, ARROW_DIRECTIONS.EAST, ARROW_DIRECTIONS.WEST]\n",
" dir_to_delta = {\n",
" ARROW_DIRECTIONS.NORTH: (-1, 0),\n",
" ARROW_DIRECTIONS.SOUTH: (1, 0),\n",
" ARROW_DIRECTIONS.EAST: (0, 1),\n",
" ARROW_DIRECTIONS.WEST: (0, -1),\n",
" }\n",
" distances = {}\n",
" for dir_enum in directions:\n",
" dist = 0\n",
" dy, dx = dir_to_delta[dir_enum]\n",
" y, x = cell.y, cell.x\n",
" while True:\n",
" y += dy\n",
" x += dx\n",
" dist += 1\n",
" if not (0 <= y < len(grid) and 0 <= x < len(grid[0])):\n",
" distances[dir_enum] = float('inf')\n",
" break\n",
" if grid[y][x].state == CellState.INSIDE:\n",
" distances[dir_enum] = dist\n",
" break\n",
" \n",
" pointing_dists = [distances[dir] for dir in cell.arrow_directions if distances[dir] != float('inf')]\n",
" if len(pointing_dists) != len(cell.arrow_directions):\n",
" return False # Some pointing direction has no INSIDE cell\n",
" if not pointing_dists:\n",
" return False # No pointing directions\n",
" min_pointing = min(pointing_dists)\n",
" if max(pointing_dists) != min_pointing:\n",
" return False # Distances not equal\n",
" \n",
" for dir_enum in directions:\n",
" if dir_enum not in cell.arrow_directions:\n",
" if distances[dir_enum] <= min_pointing:\n",
" return False # Non-pointing direction has closer or equal INSIDE\n",
" return True\n",
"\n",
"def update_grid():\n",
" for row in grid:\n",
" for cell in row:\n",
" cell.highlighted = False\n",
" \n",
" # Reset all not state_locked cells to unsure\n",
" for row in grid:\n",
" for cell in row:\n",
" if not cell.state_locked:\n",
" cell.state = CellState.UNSURE\n",
" if cell.arrow_directions:\n",
" cell.state = CellState.OUTSIDE\n",
" cell.highlighted = not is_arrow_cell_valid(cell)\n",
" if cell.value != 0:\n",
" cell.state = CellState.INSIDE\n",
" \n",
" # Find all arrows in the grid and place outside blocks directly next to them in the directions they aren't pointing.\n",
" for row in grid:\n",
" for cell in row:\n",
" if cell.arrow_directions: # has arrows\n",
" neighbours = cell.get_cardinal_neighbours(grid)\n",
" for dir_name, neigh in neighbours.items():\n",
" if neigh:\n",
" dir_enum = getattr(ARROW_DIRECTIONS, dir_name)\n",
" if dir_enum not in cell.arrow_directions:\n",
" neigh.state = CellState.OUTSIDE\n",
" \n",
" # Find all number cells and if the cell already has enough 3x3 neighbours marked INSIDE = cell.value, mark all other 3x3 neighbours as OUTSIDE.\n",
" # This should not be executed for cells that have 0 as value.\n",
" for row in grid:\n",
" for cell in row:\n",
" if cell.value > 0:\n",
" neighbourhood = cell.get_neighbourhood(grid)\n",
" inside_count = sum(1 for r in neighbourhood for c in r if c and c.state == CellState.INSIDE)\n",
" if inside_count >= cell.value:\n",
" for r in neighbourhood:\n",
" for c in r:\n",
" if c and c.state != CellState.INSIDE:\n",
" c.state = CellState.OUTSIDE\n",
" \n",
" for row in grid:\n",
" for cell in row:\n",
" if cell.arrow_directions:\n",
" cell.highlighted = not is_arrow_cell_valid(cell)\n",
" if cell.value != 0:\n",
" cell.highlighted = not is_number_cell_valid(cell)\n",
" \n",
" check_if_inside_valid()\n",
" check_if_outside_valid()"
]
},
{
"cell_type": "code",
"execution_count": 16,
"id": "cfc303d0",
"metadata": {},
"outputs": [],
"source": [
"import pygame\n",
"from pygame.locals import *\n",
"\n",
"# Initialize Pygame\n",
"pygame.init()\n",
"font = pygame.font.SysFont(None, 24)\n",
"\n",
"# Constants\n",
"CELL_SIZE = 40\n",
"WINDOW_SIZE = GRID_SIZE * CELL_SIZE\n",
"FPS = 60\n",
"\n",
"# Colors for cell states\n",
"CELL_COLORS = [\n",
" (0, 0, 0, 0), # UNSURE: transparent\n",
" (255, 255, 255, 255), # OUTSIDE: white\n",
" (0, 255, 0, 255), # INSIDE: green\n",
" (255, 255, 0, 255), # POSSIBLE: yellow\n",
" (0, 0, 255, 255), # ARROW: blue\n",
"]\n",
"\n",
"# Arrow directions offsets\n",
"ARROW_OFFSETS = {\n",
" ARROW_DIRECTIONS.NORTH: (0, -CELL_SIZE // 2 * 0.95),\n",
" ARROW_DIRECTIONS.SOUTH: (0, CELL_SIZE // 2 * 0.95),\n",
" ARROW_DIRECTIONS.EAST: (CELL_SIZE // 2 * 0.95, 0),\n",
" ARROW_DIRECTIONS.WEST: (-CELL_SIZE // 2 * 0.95, 0),\n",
"}\n",
"\n",
"\n",
"\n",
"# Set up display\n",
"screen = pygame.display.set_mode((WINDOW_SIZE, WINDOW_SIZE))\n",
"pygame.display.set_caption(\"Grid Display\")\n",
"clock = pygame.time.Clock()\n",
"\n",
"def draw_grid():\n",
" for row in grid:\n",
" for cell in row:\n",
" x, y = cell.x * CELL_SIZE, cell.y * CELL_SIZE\n",
" rect = pygame.Rect(x, y, CELL_SIZE, CELL_SIZE)\n",
" \n",
" # Draw cell background if not transparent\n",
" color = CELL_COLORS[cell.state.value]\n",
" if color[3] > 0: # Not transparent\n",
" pygame.draw.rect(screen, color[:3], rect)\n",
" \n",
" # Draw border (red if highlighted)\n",
" border_color = (255, 0, 0) if cell.highlighted else (0, 0, 0)\n",
" pygame.draw.rect(screen, border_color, rect, 2)\n",
" \n",
" # Draw arrows\n",
" center_x, center_y = x + CELL_SIZE // 2, y + CELL_SIZE // 2\n",
" for direction in cell.arrow_directions:\n",
" dx, dy = ARROW_OFFSETS[direction]\n",
" end_x, end_y = center_x + dx, center_y + dy\n",
" pygame.draw.line(screen, (255, 0, 0), (center_x, center_y), (end_x, end_y), 2)\n",
" \n",
" # Draw value if not 0\n",
" if cell.value != 0:\n",
" text = font.render(str(cell.value), True, (0, 0, 0))\n",
" text_rect = text.get_rect(center=(x + CELL_SIZE // 2, y + CELL_SIZE // 2))\n",
" screen.blit(text, text_rect)\n"
]
},
{
"cell_type": "code",
"execution_count": 17,
"id": "c996a0e6",
"metadata": {},
"outputs": [],
"source": [
"import pickle\n",
"import os\n",
"\n",
"SAVE_PATH = 'grid_editor_save.pkl'\n",
"\n",
"# Load grid if save file exists\n",
"if os.path.exists(SAVE_PATH):\n",
" with open(SAVE_PATH, 'rb') as f:\n",
" grid = pickle.load(f)\n",
"\n",
"# Editor state variables\n",
"hovered_cell = None\n",
"\n",
"# Editor to make creating the grid easier\n",
"running = True\n",
"while running:\n",
" for event in pygame.event.get():\n",
" if event.type == QUIT:\n",
" # Save grid on quit\n",
" with open(SAVE_PATH, 'wb') as f:\n",
" pickle.dump(grid, f)\n",
" running = False\n",
" elif event.type == MOUSEMOTION:\n",
" mx, my = event.pos\n",
" cell_x = mx // CELL_SIZE\n",
" cell_y = my // CELL_SIZE\n",
" if 0 <= cell_x < GRID_SIZE and 0 <= cell_y < GRID_SIZE:\n",
" hovered_cell = grid[cell_y][cell_x]\n",
" else:\n",
" hovered_cell = None\n",
" elif event.type == KEYDOWN:\n",
" if hovered_cell:\n",
" # Set value with number keys\n",
" if event.key in [K_0, K_1, K_2, K_3, K_4, K_5, K_6, K_7, K_8, K_9]:\n",
" hovered_cell.value = int(event.unicode)\n",
" elif event.key == K_w:\n",
" dir = ARROW_DIRECTIONS.NORTH\n",
" if dir in hovered_cell.arrow_directions:\n",
" hovered_cell.arrow_directions.remove(dir)\n",
" else:\n",
" hovered_cell.arrow_directions.add(dir)\n",
" elif event.key == K_a:\n",
" dir = ARROW_DIRECTIONS.WEST\n",
" if dir in hovered_cell.arrow_directions:\n",
" hovered_cell.arrow_directions.remove(dir)\n",
" else:\n",
" hovered_cell.arrow_directions.add(dir)\n",
" elif event.key == K_s:\n",
" dir = ARROW_DIRECTIONS.SOUTH\n",
" if dir in hovered_cell.arrow_directions:\n",
" hovered_cell.arrow_directions.remove(dir)\n",
" else:\n",
" hovered_cell.arrow_directions.add(dir)\n",
" elif event.key == K_d:\n",
" dir = ARROW_DIRECTIONS.EAST\n",
" if dir in hovered_cell.arrow_directions:\n",
" hovered_cell.arrow_directions.remove(dir)\n",
" else:\n",
" hovered_cell.arrow_directions.add(dir)\n",
" \n",
" screen.fill((200, 200, 200)) # Background color\n",
" draw_grid()\n",
" pygame.display.flip()\n",
" clock.tick(FPS)"
]
},
{
"cell_type": "code",
"execution_count": 18,
"id": "787f0e71",
"metadata": {},
"outputs": [],
"source": [
"def show_grid(grid):\n",
" update_grid()\n",
"\n",
" running = True\n",
" while running:\n",
" for event in pygame.event.get():\n",
" if event.type == QUIT:\n",
" running = False\n",
" elif event.type == MOUSEBUTTONDOWN:\n",
" mx, my = pygame.mouse.get_pos()\n",
" cell_x = mx // CELL_SIZE\n",
" cell_y = my // CELL_SIZE\n",
" if 0 <= cell_x < GRID_SIZE and 0 <= cell_y < GRID_SIZE:\n",
" cell = grid[cell_y][cell_x]\n",
" if cell.state != CellState.ARROW:\n",
" current = cell.state.value\n",
" if current == 0: # UNSURE\n",
" cell.state = CellState.OUTSIDE\n",
" cell.state_locked = True\n",
" elif current == 1: # OUTSIDE\n",
" cell.state = CellState.INSIDE\n",
" cell.state_locked = True\n",
" elif current == 2: # INSIDE\n",
" cell.state = CellState.UNSURE\n",
" cell.state_locked = False\n",
" \n",
" update_grid()\n",
" \n",
" screen.fill((200, 200, 200))\n",
" draw_grid()\n",
" pygame.display.flip()\n",
" clock.tick(FPS)\n",
"\n",
" pygame.quit()\n",
" return grid\n",
"\n",
"# Save grid\n",
"# with open(SAVE_PATH, 'wb') as f:\n",
"# pickle.dump(show_grid(grid), f)"
]
},
{
"cell_type": "code",
"execution_count": 19,
"id": "01a15138",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Solving...\n",
"Found solution 1\n",
"Found solution 2\n",
"Found solution 3\n",
"Found solution 4\n",
"Found solution 5\n",
"Found solution 6\n",
"Found solution 7\n",
"Found solution 8\n",
"Found solution 9\n",
"Found solution 10\n",
"Found solution 11\n",
"Found solution 12\n",
"Found solution 13\n",
"Found solution 14\n",
"Found solution 15\n",
"Found solution 16\n",
"Found solution 17\n",
"Found solution 18\n",
"Found solution 19\n",
"Found solution 20\n",
"Found solution 21\n",
"Found solution 22\n",
"Found solution 23\n",
"Found solution 24\n",
"Found solution 25\n",
"Found solution 26\n",
"Found solution 27\n",
"Found solution 28\n",
"Found solution 29\n",
"Found solution 30\n",
"Found solution 31\n",
"Found solution 32\n",
"Found solution 33\n",
"Found solution 34\n",
"Found solution 35\n",
"Found solution 36\n",
"Found solution 37\n",
"Found solution 38\n",
"Found solution 39\n",
"Found solution 40\n",
"Found solution 41\n",
"Found solution 42\n",
"Found solution 43\n",
"Found solution 44\n",
"Found solution 45\n",
"Found solution 46\n",
"Found solution 47\n",
"Found solution 48\n",
"Found solution 49\n",
"Found solution 50\n",
"Found solution 51\n",
"Found solution 52\n",
"Found solution 53\n",
"Found solution 54\n",
"Found solution 55\n",
"Found solution 56\n",
"Found solution 57\n",
"Found solution 58\n",
"Found solution 59\n",
"Found solution 60\n",
"Found solution 61\n",
"Found solution 62\n",
"Found solution 63\n",
"Found solution 64\n",
"Found solution 65\n",
"Found solution 66\n",
"Found solution 67\n",
"Found solution 68\n",
"Found solution 69\n",
"Found solution 70\n",
"Found solution 71\n",
"Found solution 72\n",
"Total solutions found: 72\n"
]
}
],
"source": [
"from z3 import *\n",
"\n",
"ROWS = 20\n",
"COLS = 20\n",
"\n",
"# Parse clues\n",
"arrows = {}\n",
"numbers = {}\n",
"\n",
"for y in range(GRID_SIZE):\n",
" for x in range(GRID_SIZE):\n",
" c = grid[y][x]\n",
" r = y\n",
" col = x\n",
" if c.arrow_directions:\n",
" arrows[(r, col)] = set(dir.name for dir in c.arrow_directions)\n",
" if c.value != 0:\n",
" numbers[(r, col)] = c.value\n",
"\n",
"\n",
"# Function to check whether a cell is inside\n",
"def is_in_grid(row, col):\n",
" return 0 <= row < ROWS and 0 <= col < COLS\n",
" \n",
"\n",
"def solve_all_grids():\n",
" s = Solver()\n",
" \n",
" # Initialize the grid as ints (could have been booleans but numbers make later constraints easier to model)\n",
" grid = [[Int(f\"g_{r}_{c}\") for c in range(COLS)] for r in range(ROWS)]\n",
" \n",
" # Constrain each int to 0,1\n",
" for r in range(ROWS):\n",
" for c in range(COLS):\n",
" s.add(grid[r][c] >= 0, grid[r][c] <= 1)\n",
"\n",
" # All arrows are outside (0), all numbers are inside (1)\n",
" for (r,c) in arrows: s.add(grid[r][c] == 0)\n",
" for (r,c) in numbers: s.add(grid[r][c] == 1)\n",
"\n",
" # Constraints for the neighbor counts\n",
" for (r,c), val in numbers.items():\n",
" neighs = []\n",
" for dr in (-1,0,1):\n",
" for dc in (-1,0,1):\n",
" rr, cc = r+dr, c+dc\n",
" if is_in_grid(rr, cc):\n",
" neighs.append(grid[rr][cc])\n",
" s.add(Sum(neighs) == val)\n",
"\n",
" # Arrow constraints\n",
" # Helper to get distance expression by building a ray of Ifs\n",
" # It walks backwards from the edge to the cell, building an If chain\n",
" # the chain reads if the current cell is inside, return distance, else (if chain)\n",
" def get_dist_expr(row, col, dx, dy):\n",
" \n",
" # Build a list of cells along the specified direction\n",
" cells = []\n",
" curr_row, curr_col = row + dx, col + dy\n",
" while is_in_grid(curr_row, curr_col):\n",
" cells.append((curr_row, curr_col))\n",
" curr_row += dx\n",
" curr_col += dy\n",
" \n",
" # Start with an arbitrary large distance\n",
" if_chain = 999\n",
" \n",
" # Iterate backwards to build the If chain, otherwise the last element would have priority\n",
" for i in range(len(cells)-1, -1, -1):\n",
" rr, cc = cells[i]\n",
" dist = i + 1\n",
" # If the cell is inside, return distance, else continue the chain\n",
" if_chain = If(grid[rr][cc] == 1, dist, if_chain)\n",
" return if_chain\n",
"\n",
" dir_map = {\"NORTH\": (-1, 0), \"SOUTH\": (1, 0), \"EAST\": (0, 1), \"WEST\": (0, -1)}\n",
" \n",
" for (r,c), dirs in arrows.items():\n",
" # Define the target distance of the arrow\n",
" target = Int(f\"arrow_target_{r}_{c}\")\n",
" \n",
" s.add(target > 0, target < GRID_SIZE)\n",
" \n",
" for d_name, (dx, dy) in dir_map.items():\n",
" dist_expr = get_dist_expr(r, c, dx, dy)\n",
" \n",
" # If the arrow points in this direction, distance must equal target\n",
" # Else distance must be greater than target\n",
" if d_name in dirs:\n",
" s.add(dist_expr == target)\n",
" else:\n",
" s.add(dist_expr > target)\n",
"\n",
" # Constraint to force all inside cells to be connected\n",
" # Select the first number cell as root (since it is an inside cell per definition), so all inside cells must connect to it\n",
" root_r, root_c = list(numbers.keys())[0]\n",
" \n",
" # Idea:\n",
" # We check connectivity by essentially doing a flood fill with distance values\n",
" # Then if a cell is inside it must have a cardinal neighbor with dist = d-1 otherwise there does not exist a path to the root\n",
" \n",
" # Create a new distance grid for connectivity\n",
" d_in = [[Int(f\"d_in_{r}_{c}\") for c in range(COLS)] for r in range(ROWS)]\n",
" \n",
" for r in range(ROWS):\n",
" for c in range(COLS):\n",
" # If outside, dist is -1\n",
" s.add(Implies(grid[r][c] == 0, d_in[r][c] == -1))\n",
" \n",
" # If the cell is the root cell, set the distance to 0\n",
" if (r,c) == (root_r, root_c):\n",
" s.add(d_in[r][c] == 0)\n",
" continue\n",
" \n",
" # Since the cell is not the root cell, its distance must be > 0 if inside\n",
" s.add(Implies(grid[r][c] == 1, d_in[r][c] > 0))\n",
" \n",
" # Get the cardinal neighbors\n",
" neighs = []\n",
" for dr, dc in [(0,1), (0,-1), (1,0), (-1,0)]:\n",
" rr, cc = r+dr, c+dc\n",
" if is_in_grid(rr, cc):\n",
" neighs.append(d_in[rr][cc])\n",
" \n",
" # Since the cell is inside, there must exist a neighbor with dist = d-1\n",
" s.add(Implies(grid[r][c] == 1, Or([n == d_in[r][c] - 1 for n in neighs])))\n",
"\n",
" # Connected to edge constraint\n",
" # Create a new distance grid for outside connectivity\n",
" d_out = [[Int(f\"d_out_{r}_{c}\") for c in range(COLS)] for r in range(ROWS)]\n",
" \n",
" # Idea:\n",
" # If a cell is on the outside and on the boundary, dist = 0\n",
" # If a cell is outside and not on the boundary, there must exist a neighbor with dist = d-1\n",
" \n",
" for r in range(ROWS):\n",
" for c in range(COLS):\n",
" s.add(Implies(grid[r][c] == 1, d_out[r][c] == -1))\n",
" s.add(Implies(grid[r][c] == 0, d_out[r][c] >= 0))\n",
" \n",
" is_boundary = (r == 0 or r == ROWS-1 or c == 0 or c == COLS-1)\n",
" \n",
" if is_boundary:\n",
" s.add(Implies(grid[r][c] == 0, d_out[r][c] == 0))\n",
" continue\n",
" \n",
" # If outside and not boundary, dist > 0\n",
" s.add(Implies(grid[r][c] == 0, d_out[r][c] > 0))\n",
" \n",
" neighs = []\n",
" for dr, dc in [(0,1), (0,-1), (1,0), (-1,0)]:\n",
" rr, cc = r+dr, c+dc\n",
" neighs.append(d_out[rr][cc])\n",
" \n",
" # If the cell is outside, then there must exist a neighbor with dist = d-1\n",
" s.add(Implies(grid[r][c] == 0, Or([n == d_out[r][c] - 1 for n in neighs])))\n",
"\n",
" print(\"Solving...\")\n",
" solutions = []\n",
" while s.check() == sat:\n",
" m = s.model()\n",
" res_grid = [[0]*COLS for _ in range(ROWS)]\n",
" for r in range(ROWS):\n",
" for c in range(COLS):\n",
" res_grid[r][c] = m.evaluate(grid[r][c]).as_long()\n",
" solutions.append(res_grid)\n",
" print(f\"Found solution {len(solutions)}\")\n",
" \n",
" # Force the next solution to be different\n",
" block = []\n",
" for r in range(ROWS):\n",
" for c in range(COLS):\n",
" val = res_grid[r][c]\n",
" block.append(grid[r][c] != val)\n",
" s.add(Or(block))\n",
" \n",
" if len(solutions) >= 100: # Safety limit\n",
" print(\"Limit reached\")\n",
" break\n",
" \n",
" print(f\"Total solutions found: {len(solutions)}\")\n",
" return solutions\n",
"\n",
"solutions = solve_all_grids()"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "5e318edc",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Grid updated with commonalities.\n"
]
}
],
"source": [
"# If a cell is 1 in all solutions -> INSIDE\n",
"# If a cell is 0 in all solutions -> OUTSIDE\n",
"# Else -> UNSURE\n",
"\n",
"for r in range(ROWS):\n",
" for c in range(COLS):\n",
" vals = [sol[r][c] for sol in solutions]\n",
" if all(v == 1 for v in vals):\n",
" grid[r][c].state = CellState.INSIDE\n",
" grid[r][c].state_locked = True\n",
" elif all(v == 0 for v in vals):\n",
" grid[r][c].state = CellState.OUTSIDE\n",
" grid[r][c].state_locked = True\n",
" else:\n",
" grid[r][c].state = CellState.UNSURE\n",
" grid[r][c].state_locked = False\n",
"\n",
"update_grid()\n",
"print(\"Grid updated with commonalities.\")"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "73f34c3b",
"metadata": {},
"outputs": [],
"source": [
"show_grid(grid)"
]
},
{
"cell_type": "markdown",
"id": "3d469d46",
"metadata": {},
"source": [
"# Solution \n",
"16.414.860, 16414860\n",
"\n",
"Side lengths 2x6x7\n",
"\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": ".venv",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.13.5"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment