[rjeli]

Nice! I rewrote it in z3 and was able to avoid the if-elses by tracking the occupancy of each cell as an integer, and constraining it to exactly 1: https://gist.github.com/rjeli/a1612da0e3c8b99ec4514e689ebdfa...

[polivier]

Well done! My CP formulation is definitely not the best here. I put this model together late one night while drinking a few beers :)