Solving Battleships with SAT
Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.
iff_gen() sets up the bidirectional if-and-only-if relationship. (Of course there is a unidirectional
if_gen() as well.) In the above example, if the point
xy is true then any of the ships connected to that point exist. And if none of those ships exist, then the point
xy must be false. The
iff_gen() function in general takes a pair of sets of terms, and each collection of terms has a "mode" of
all to determine if just one term must be true or if all of the terms must be true. There was no need to set
modeA here because there was only a single term so the any/all distinction is meaningless.