SAT: parity board

We get the following challenge:

I take "clear" to mean that all tiles should be the same color, either black or white. One "move" is to click a tile, which changes the color of it, and also its 4-connected neighbors. Illustration:

Clicking a tile changes the color of it, and its 4-connected neighbors.

This can be solved with SAT. Some analysis of the problem:

• Clicking a tile twice is the same as not clicking it at all. The only thing that matters is parity of clicks. If we assume that we are looking for an optimal solution, we can assume that each tile is clicked 0 or 1 times. So, they can be modeled as boolean variables. 
• Parity is also the only thing that matters for clearing the board. Suppose we want to make all tiles white. Then, black tiles should switch color an odd number of times. White tiles should switch color an even number of times. 
• If we can count the number of color switches each tile has done, we can add cardinality constraints on the click variables that cover each tile. 
• We also have to add a cardinality constraint on the whole set of click variables. 

For small numbers like this, we can do parity as a disjunction of equality clauses. 

This produces the following solution:

0  0  1  0  0

0  0  1  0  0

1  0  0  1  1

0  1  0  1  1

0  0  0  1  0

(1 means click this tile, 0 means no click)