Solving Battleships with SAT
Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.
The simplest requirement is that each ship appear only once out of the dozens of places it could be. The
cells list holds the terms that are related to a single ship. The
tree_one() function takes a list of terms and then constructs a binary tree out of them such that at most one of the terms will be true. The
root value of this tree will be one if any of the leaves are active, and it will be zero if none of them are. Or (as in this case) if the root is set to one then one of the leaves must also be true. The function
cnf.write_one() creates a clause from the terms it is given - here by writing a clause of a single term, that single term must be true. Additionally a summary of how many legal positions there are for each ship will be displayed. Frequently one of the ships will be extremely constrained; normally puzzles are designed this way to give a human solver a place to start.