Of course there are many ways of stating those two things. Here I take a slightly different approach. Every point has scores of possible ships that could be occupying it. If the point is filled then one of those ships must exist. And vice versa. This bidirectional relationship is crucial! Note the previous way of stating things (if a ship exists, then several points are active) is not reversible. Just because a point (or even set of consecutive points) is filled does not mean that that particular ship exists. You almost always want to set up a bidirectional relationship whenever possible. It makes the SAT solver work much more quickly as it can solve more readily in either direction. |