Update this project:
User: <input type="text" name="user"> Pass: <input type="password" name="pass">
Title:
News:
Category:
Here we'll be going through a complete listing of a solver for a type of puzzle called <a href="https://en.wikipedia.org/wiki/Battleship_(puzzle)">Battleship</a>. It is based on the classic two player board game, but with slightly different rules and information. The wikipedia link talks about it more and presents examples. You are given information about the ships present and how many tiles are occupied by ships in a given row or column. This is similar to a [nonogram](https://en.wikipedia.org/wiki/Nonogram) however it is very common for some of the counts to be missing or for partial information about the contents of a square to be provided, so this solver will incorporate those features. If you are unfamiliar with the basics of SAT, I suggest you look at [this primer](http://kmkeen.com/sat/). You may concatenate all of these segments together to produce a python script. Let's begin. #! /usr/bin/env python3 from sat import * cnf = CNF('/tmp/bs.cnf') f = cnf.auto_term I'll be using a helper library [sat.py](https://github.com/keenerd/satisfiability) quite a lot. Here `CNF` refers to [conjuctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form), the basis for how logical networks are expressed to a SAT solver. In general SAT is a very low-level tool and lacks any sort of abstraction. That makes it fast, east to reason about and easy to debug. But you very quickly miss high level features such as being able to give variables names. The `autoterm` function handles linking the names you create to the simple integer addresses that SAT uses internally. We'll be using it a lot so it gets a single-letter in the global space. Next the puzzle is typed up. ships = '+++++ ++++ ++++ +++ +++ +++ ++ ++ ++ ++ + + + +' across = '4 4 3 1 5 1 2 6 2 1 1 1 2 1 0' down = '1 1 2 4 1 1 2 3 4 1 5 1 3 4 1' puzzle = """\ ............... ............... ............... ............#>. ..v............ ............... ............O.. .......^....... #...v....O..... ............... ......#........ .^............. ........^...... ....v.O........ ...............""" I'm sure some people won't be happy to see this hard-coded into the sources. But writing parsers is annoying for toy problems. And in an actual Puzzle Hunt you will be presented with a unique variation that will require many one-off modifications to the sources anyway. First the ships are listed graphically. Then the clues are given. The `across` string reads the numbers across the top from left to right, and `down` reads the numbers from the left side from top to bottom. Finally the givens on the puzzle board are presented as ASCII art. Of course all of that was made to be easy to type up and fast to proof-check. It doesn't do the computer any good and that artwork needs to be transformed into an equivalent table of information puzzle = [list(line) for line in puzzle.split()] xs = list(range(len(puzzle[0]))) ys = list(range(len(puzzle))) table = dict(((x,y),puzzle[y][x]) for x,y in product(xs,ys)) ships = dict((str(i),s) for i,s in enumerate(ships.split())) in_bounds = set(product(xs,ys)) symbols = '. ~ O # < > v ^'.split() maybe_int = lambda s: '?' if s is '?' else int(s) across = [maybe_int(n) for n in across.split()] down = [maybe_int(n) for n in down.split()] if '?' not in across: assert sum(across) == sum(len(s) for s in ships.values()) if '?' not in down: assert sum(down) == sum(len(s) for s in ships.values()) * `xs` and `ys` contain the row and column numbers, treating the upper left as the origin. * `table` is a dictionary mapping `(x,y)` tuples to the ASCII-art puzzle board. * `ships` gives each of the ships a numeric ID and records the length for later use. * `in_bounds` is a set of `(x,y)` points. If the puzzle had ragged edges or holes in the board, remove them here. * `symbols` will be used later to sanity-check the typed up puzzle. * The final section converts `across` and `down` to lists of integers, with a provision for unknowns and a quick sanity check. ## Useful Functions Now we can actually dig into solving the puzzle. First though is the internal representation of the puzzle. There are many ways to do this but I've elected to largely disregard that the puzzle takes place on a board and instead focus on where the ships are. That is, each ship can be in a large number of places. But it can only be in one place at a time and when it is in that place, other ships won't be able to occupy nearby or overlapping positions. To solve the puzzle, every one of these interactions will be recorded and any combinations that don't collide must be a solution. So where a ship is and what a ship is are very important. Each ship has it's unique identifier, an `(x,y)` point where it begins at, it's size, and a direction that it is pointing. I chose to represent this as a five-element tuple for compactness but a lightweight Object would not have been out of the question. def every_ship(prefix, size): for x1,y1,d in product(xs, ys, 'SE'): if size == 1 and d == 'S': continue if d == 'E' and x1 + (size-1) not in xs: continue if d == 'S' and y1 + (size-1) not in ys: continue yield prefix, x1, y1, size, d Given the length of a ship, `every_ship()` produces every possible place it could be. It is also useful to know what points on the grid would be occupied by a ship at a certain location. These are produced by `just_ship()`. There are a relatively small number of locations and this ends up being one of the slowest and most frequently called parts of the code, so the results are memoized. def just_ship(prefix, x1, y1, size, d, cache={}): "prefix is ignored" if (x1, y1, size, d) in cache: return cache[(x1, y1, size, d)] if d == 'E': points = [(x1+i,y1) for i in range(size)] elif d == 'S': points = [(x1,y1+i) for i in range(size)] else: raise cache[(x1, y1, size, d)] = points return points Similarly it is useful to know the immediate area around a ship since other ships can't occupy that space. Though this is called less often and caching isn't required. def just_water(points): water = set((xy[0]+xo, xy[1]+yo) for xy,xo,yo in product(points, [-1,0,1], [-1,0,1])) water = (water - set(points)) & in_bounds return water And then to go full-circle, these tuples describing a ship can be turned back into ASCII-art representations with the `exact_ship()` function. This will only be used in two places: checking if a ship would disagree with an initial clue and pretty-printing the final puzzle solution. def exact_ship(prefix, x1, y1, size, d): "prefix is ignored" points = just_ship(None, x1, y1, size, d) water = [[xy,'~'] for xy in just_water(points)] points = [[xy,'#'] for xy in points] if size == 1: points[0][1] = 'O' if size >= 2 and d == 'E': points[0][1] = '<' points[-1][1] = '>' if size >= 2 and d == 'S': points[0][1] = '^' points[-1][1] = 'v' return dict(points + water) Finally we can make every possible ship very simply: def generate_all_ships(ships): for i,ship in ships.items(): for s in every_ship(i, len(ship)): yield s Of course some of these locations for ships are clearly illegitimate with the given clues. These are removed by `filter_givens()`. def filter_givens(all_ships): "remove ships that conflict with board givens" knowns = set(xy for xy in table if table[xy] != '.') for ship1 in all_ships: points = exact_ship(*ship1) okay = not any(points[xy] != table[xy] for xy in knowns & set(points)) if okay: yield ship1 And it is also impossible for a long ship to exist in a row without enough tallies to accommodate it. Nor for any ship to exist in a zero row. def filter_tallies(all_ships): "remove ships that conflict with tallies" for ship1 in all_ships: # prefix, x1, y1, size, d _,_,_,size,d = ship1 points = just_ship(*ship1) okay = True for x,y in points: if across[x] == '?': continue if down[y] == '?': continue if across[x] == 0: okay = False if down[y] == 0: okay = False if d == 'E' and down[y] < size: okay = False if d == 'S' and across[x] < size: okay = False if okay: yield ship1 All of these functions are chained together to produce the master list of `all_ships`: all_ships = list(filter_givens(filter_tallies(generate_all_ships(ships)))) ## Primary logic This is the real meat of the solver. Here the CNF is assembled. Comments are interspersed into the CNF to [facilitate debugging](http://kmkeen.com/sat-debugging/). cnf.comment('declare ships') cnf.auto_mode = 'wo' for prefix, x1, y1, size, d in all_ships: f(prefix, x1, y1, size, d) cnf.comment('declare board') for x,y in product(xs, ys): f(x,y) cnf.auto_mode = 'ro' The very first part of making a CNF is to make all (or at least most) of the variables. Setting `auto_mode` to write-only ensures that every created label is unique. Calling `f()` with the label's values creates the label, assigns it a numbered term and returns that number. Though here we don't need the numbers, so the return value is ignored. One term is made for every possible ship position and also the squares of the main board. This representation of the board will be used for enforcing the row/column tallies. cnf.comment('each ship once') line = '' for i in ships: cells = [f(*stuff) for stuff in all_ships if stuff[0] == i] line += '%s %i, ' % (ships[i], len(cells)) root = tree_one(cnf, 'each ship once - %s' % i, cells) cnf.write_one(root) print(line) The simplest requirement is that each ship appear only once out of the dozens of places it could be. The `cells` list holds the terms that are related to a single ship. The `tree_one()` function takes a list of terms and then constructs a binary tree out of them such that at most one of the terms will be true. The `root` value of this tree will be one if any of the leaves are active, and it will be zero if none of them are. Or (as in this case) if the root is set to one then one of the leaves must also be true. The function `cnf.write_one()` creates a clause from the terms it is given - here by writing a clause of a single term, that single term must be true. Additionally a summary of how many legal positions there are for each ship will be displayed. Frequently one of the ships will be *extremely* constrained; normally puzzles are designed this way to give a human solver a place to start. What follows is probably the most complicated section of code. No ships are allowed to overlap, or be too close to each other. Normally I would use `combinations(all_ships, 2)` to go through all the pairs of ships but nested `for` loops allows for easier re-use of the `points1` and `water1` sets. cnf.comment('no overlapping ships') for i,ship1 in enumerate(all_ships): points1 = set(just_ship(*ship1)) water1 = just_water(points1) occupied1 = points1 | water1 for ship2 in all_ships[i:]: if ship1[0] == ship2[0]: continue points2 = set(just_ship(*ship2)) if occupied1 & points2: cnf.write_one(-f(*ship1), -f(*ship2)) # (points1 & water2) would be redundant Sets of points are extremely convenient to work with! Intersections, unions and differences are fast and concise. Note the use of `write_one(-f(*ship1), -f(*ship2))` above. The `f()` of course turns the ship tuple into a term number. Writing a pair of negative numbers to a clause means that it is impossible for both terms to be simultaneously true. Otherwise, (-true, -true) evaluates to (false, false) and the CNF is unsatisfiable. Now for something conceptually simpler, that I manage to make seem complicated. cnf.comment('link ships to board') covered = defaultdict(list) for ship1 in all_ships: for xy in just_ship(*ship1): covered[xy].append(ship1) for xy in in_bounds: cells = [f(*s) for s in covered[xy]] if not cells: cnf.write_one(-f(*xy)) continue cnf.write(iff_gen(f(*xy), cells, modeB=any)) Every ship will cover some points on the board. If a particular ship is in a particular location, then the points it occupies must be filled. If it is not possible to put any ships over a given point, then that point must be empty. Of course there are many ways of stating those two things. Here I take a slightly different approach. Every point has scores of possible ships that could be occupying it. If the point is filled then one of those ships must exist. And vice versa. This bidirectional relationship is crucial! Note the previous way of stating things (if a ship exists, then several points are active) is not reversible. Just because a point (or even set of consecutive points) is filled does not mean that *that particular ship* exists. You almost always want to set up a bidirectional relationship whenever possible. It makes the SAT solver work much more quickly as it can solve more readily in either direction. The `iff_gen()` sets up the bidirectional if-and-only-if relationship. (Of course there is a unidirectional `if_gen()` as well.) In the above example, if the point `xy` is true then any of the ships connected to that point exist. And if none of those ships exist, then the point `xy` must be false. The `iff_gen()` function in general takes a pair of sets of terms, and each collection of terms has a "mode" of `any` or `all` to determine if just one term must be true or if all of the terms must be true. There was no need to set `modeA` here because there was only a single term so the any/all distinction is meaningless. cnf.comment('apply simple givens') for x,y in in_bounds: if table[(x,y)] == '.': continue if table[(x,y)] == '~': cnf.write_one(-f(x,y)) continue # other symbols cnf.write_one(f(x,y)) That part was straightforward. If a point is water, then it can't be occupied by a ship. If a point is occupied by a ship, then it is occupied by a ship. Most of the points are unknown, and those can be skipped over. cnf.comment('apply clues to board') for x in xs: if across[x] == '?': continue cells = [f(x,y) for y in ys] cnf.write(window(cells, across[x], across[x])) for y in ys: if down[y] == '?': continue cells = [f(x,y) for x in xs] cnf.write(window(cells, down[y], down[y])) And finally those row/column tallies from the very beginning are applied to the board. `window()` sets up that a certain minimum and maximum of terms in a set of terms are true. ## Conclusion At this point the entire puzzle has been expressed as a giant boolean logical expression. All that is left to do is report the results. print('terms:', cnf.maxterm) print('clauses:', cnf.clauses) assert cnf.verify() interesting = set(f(x,y) for x,y in product(xs, ys)) for solution in cnf.solutions(3, interesting=interesting): print() marked = {} used_ships = [s for s in all_ships if f(*s) in solution] for s in used_ships: marked.update(exact_ship(*s)) for y in ys: line = '' for x in xs: if (x,y) in marked: line += marked[(x,y)] else: line += '.' line += ' ' line = line.replace('~', '.') print(line) Usually I will look for three solutions. Typically I only care if there are zero, one, two, or many solutions. The `interesting` points are a small subset that summarizes the entire solution. Normally it is used to help eliminate trivial duplicates. For example, there are multiple boats of each length. If you consider *all* of the terms to be part of the answer, then two ships that have swapped position will be a unique answer, despite the resulting board being identical. Here is the output it produces for this puzzle: +++++ 11, ++++ 26, ++++ 26, +++ 40, +++ 40, +++ 40, ++ 89, ++ 89, ++ 89, ++ 89, + 117, + 117, + 117, + 117, terms: 2225 clauses: 93443 . . . . . . . ^ . . . . . . . . . . . . . . # . . . . . . . . . ^ . . . . v . . . . . . . . . # . . . . . . . . < # > . . . v . . . . . . . . . . . . . . . . . . . . . . O . . . . ^ . . . . . . . . . . . O . . # . . . ^ . . ^ . . . . . . . # . . . v . . v . O . . . . . v . . . . . . . . . . . . . . . . . < # # # > . . . . . . . . ^ . . . . . . . . . . . . . . # . . ^ . . . ^ . . . . . . . # . . v . O . v . . . . . . . v . . . . . . . . . . . . . And that completes the battleship solver. It is pretty easy to extend for more complicated variants. It already supports missing tallies and I hinted at how it could handle boards with holes in them. At the Mystery Hunt it was smashed together with a few other solvers I had on hand for [Shoal Patrol](http://web.mit.edu/puzzle/www/2018/full/puzzle/shoal_patrol.html), probably the wildest Battleship variant I've ever seen.
Preview