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
I suppose it is tempting, if the only tool you have is a
hammerSAT solver, to treat everything as if it were a nailSAT problem.
CNF Encoding Aztec Puzzles
What are the encoding rules? It works! ...on small puzzles...
Still too big!
A better encoding. Knuth, Sinz
Success! Next up....the 400 piece puzzle.
© 2020 Jordan Ford