Solving Battleships with SAT

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

Note the use of write_one(-f(*ship1), -f(*ship2)) above. The f() of course turns the ship tuple into a term number. Writing a pair of negative numbers to a clause means that it is impossible for both terms to be simultaneously true. Otherwise, (-true, -true) evaluates to (false, false) and the CNF is unsatisfiable.

Mail: (not shown)

Please type this: