assign(domain_size,64).
assign(max_models,1).
set(arithmetic).

list(distinct).
 [a0,  a1,  a2,  a3,  a4,  a5,  a6,  a7,  a8,  a9, 
  a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,
  a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31,
  b0,  b1,  b2,  b3,  b4,  b5,  b6,  b7,  b8,  b9, 
  b10, b11, b12, b13, b14, b15, b16, b17, b18, b19,
  b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]. 
end_of_list.

formulas(utils).
  left(x,y) <-> x mod 8 !=7 & y = x + 1. 
  on(x,y)   <-> x < 56 & y = x + 8.
end_of_list.

formulas(black_white).
  left(x,y) & w(x) -> b(y). %adjacent squares have different colors
  left(x,y) & b(x) -> w(y).    
  on(x,y) & b(x) -> w(y).
  on(x,y) & w(x) -> b(y).

  w(x) <-> x=0  | x=2  | x=4  | x=6  | x=9  | x=11 | x=13 | x=15 |
           x=16 | x=18 | x=20 | x=22 | x=25 | x=27 | x=29 | x=31 |
           x=32 | x=34 | x=36 | x=38 | x=41 | x=43 | x=45 | x=47 |
           x=48 | x=50 | x=52 | x=54 | x=57 | x=59 | x=61 | x=63.
  w(x) <-> -b(x).  % if white not black

  w(a0).  w(a1).  w(a2).  w(a3).  w(a4).  w(a5).  w(a6).   w(a7).    
  w(a8).  w(a9).  w(a10). w(a11). w(a12). w(a13). w(a14).  w(a15).   
  w(a16). w(a17). w(a18). w(a19). w(a20). w(a21). w(a22).  w(a23).
  w(a24). w(a25). w(a26). w(a27). w(a28). w(a29). w(a30).  w(a31).

  b(b0).  b(b1).  b(b2).  b(b3).  b(b4).  b(b5).  b(b6).   b(b7).    
  b(b8).  b(b9).  b(b10). b(b11). b(b12). b(b13). b(b14).  b(b15).   
  b(b16). b(b17). b(b18). b(b19). b(b20). b(b21). b(b22).  b(b23).
  b(b24). b(b25). b(b26). b(b27). b(b28). b(b29). b(b30).  b(b31).
end_of_list.

formulas(shapes).
  p1  -> left(b0,a0)   & on(b1,a0).
  p2  -> left(b2,a1)   & on(b3,a1).
  p3  -> left(a3,b4)   & on(b4,a2).
  p4  -> left(b5,a5)   & on(b5,a4)   & on(b6,a5).
  p5  -> left(b7,a7)   & on(b7,a6)   & on(b8,a7).
  p6  -> left(b9,a9)   & on(b9,a8)   & on(b10,a9)    & on(a10,b10).
  p7  -> left(a12,b12) & on(b12,a11) & on(a11,b11).
  p8  -> left(b13,a13) & on(b14,a13) & left(b14,a14).
  p9  -> left(a16,b16) & on(b16,a15) & left(a15,b15). 
  p10 -> left(a19,b19) & on(b19,a18) & on(a18,b17)   & on(b18,a17) & 
         left(a18,b18).
  p11 -> left(b21,a21) & on(a22,b21) & on(b21,a20)   & on(a20,b20).
  p12 -> left(b22,a25) & on(b22,a23) & on(b24,a25)   & left(a25,b23) & 
         left(b23,a26) & on(b23,a24) & on(b25,a26).
  p13 -> left(b28,a29) & on(b29,a29) & on(a29,b27)   & left(b27,a28) & 
         left(b26,a27) & on(b27,a27).   
  p14 -> left(a31,b31) & on(a31,b30) & on(b30,a30).

  p1. p2. p3. p4. p5. p6. p7. p8. p9. p10. p11. p12. p13. p14. 
end_of_list.

formulas(help).
 on(a2,b23)  | on(a4,b23) | on(a6,b23) | on(a8,b23) | on(a30,b23). %pos i
 on(a25,b3)  | on(a25,b6) | on(a25,b8) | on(a25,b29).              %pos j 
 on(b28,a14) | on(b28,a21).                                        %pos k
 a31 =  0.  b31 =  1.  b30 =  8.  a30 = 16.              %top-left corner
 a0  = 63.  b0  = 62.  b1  = 55.                     %bottom-right corner
 a3  mod 8 != 0.     a12 mod 8 != 0.     %p3 and p7 cannot be on column 0 
 a16 mod 8 != 0.     a19 mod 8 != 0.    %p9 and p10 cannot be on column 0 
end_of_list.





