I'll be using a helper library sat.py quite a lot. Here CNF
refers to conjuctive normal form, the basis for how logical networks are expressed to a SAT solver. In general SAT is a very lowlevel 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 singleletter in the global space.
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 hardcoded 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 oneoff 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 proofcheck. 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
andys
contain the row and column numbers, treating the upper left as the origin. 
table
is a dictionary mapping(x,y)
tuples to the ASCIIart 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 sanitycheck the typed up puzzle. 
The final section converts
across
anddown
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 fiveelement 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 + (size1) not in xs:
continue
if d == 'S' and y1 + (size1) 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 fullcircle, these tuples describing a ship can be turned back into ASCIIart 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 prettyprinting 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 writeonly 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 reuse 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 ifandonlyif 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.
easy to reason