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 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 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.