SAT Solving Aztec Puzzles
Jordan S. Ford

Aztec Puzzles

The best gifts send a subtle message to their recipient. A 36" Gränsfors Bruks American Felling Axe says "Dear husband, I think you're a sexy viking who deserves a $250 Scandinavian axe, even though you're a computer nerd, not an alpine lumberjack."

The worst gifts send a message too.

This is the Aztec Puzzle. It says, "Dear Son-In-Law, we both know you have nothing better to do than spend 5000 hours on mindless O(n2) tasks, so here's a crappy lasercut puzzle, you lazy piece of crap. When are you gonna get a real job?"

No time soon!

In this article, we're going to use computers to solve Aztec puzzles, so we don't have to. We'll search for an efficient encoding to translate Aztec puzzles into Boolean Satisfiability problems. Then, we'll use a modern SAT solver to solve them for us, permanently freeing us from an entire class of Christmas and birthday torture devices.

Brute Force Search

When faced with a problem like the Aztec puzzle, brute force search is a natural place to start. In the case of the aztec puzzle, we could search all permutations of the pieces until we found a solution. In pseudocode that might look something like this:


  def brute_force_aztec():
    for p1 in puzzle_locations X piece_rotations:
      if fits_in_puzzle(p1):
        for p2 in puzzle_locations X piece_rotations:
          if fits_in_puzzle(p1, p2):
            ...
            for pN in puzzle_locations X piece_rotations:
              if fits_in_puzzle(p1, p2, ..., pN):
                return [p1, p2, ..., pN]
      return NO_SOLUTION

With a nested for-loop for every piece, it should be obvious that this solution will not scale beyond a small handful of pieces. For the 51 piece puzzle shown above, this solution would evaluate as many as (29 rows * 30 columns * 4 rotations)51 pieces or about
4173894247253222141003397955065691624478788188493738037751463069185887231638945125788726316601346256717097551739783768781359153152000000000000000000000000000000000000000000000000000
possible solutions. Even with some clever pruning strategies, that's not going to work!

Boolean Satisfiability


I suppose it is tempting, if the only tool you have is a  hammer  SAT solver, to treat everything as if it were a  nail  SAT problem.

CNF Encoding Aztec Puzzles

What are the encoding rules? It works! ...on small puzzles...

Too big!

Deduplicate.

Still too big!

A better encoding. Knuth, Sinz

Success!

Success! Next up....the 400 piece puzzle.


© 2020 Jordan Ford