Solving Battleships with SAT

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

I'll be using a helper library 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 low-level 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 single-letter in the global space.

Mail: (not shown)

Please type this: