Battleship

Here we'll be going through a complete listing of a solver for a type of puzzle called Battleship. 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 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.

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

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.

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.

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, probably the wildest Battleship variant I've ever seen.