Solving Battleships with SAT

Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

  • 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.
Mail: (not shown)

Please type this: