var x{i in 1..9, j in 1..9, k in 1..9}, binary;
/* x[i,j,k] is 1 iff in the ith column (from the left) in the jth row (from the bottom) there is a k */

var y{i in 1..9, j in 1..9}, integer, >=1, <=9;


s.t. one_per_entry{i in 1..9, j in 1..9}: sum{k in 1..9} x[i,j,k] = 1;
s.t. one_per_row{j in 1..9, k in 1..9}: sum{i in 1..9} x[i,j,k] = 1;
s.t. one_per_column{i in 1..9, k in 1..9}: sum{j in 1..9} x[i,j,k] = 1;
s.t. one_per_block{i1 in 1..3, j1 in 1..3, k in 1..9}: sum{i2 in 1..3, j2 in 1..3} x[3*i1 + 1 - i2, 3*j1 + 1 - j2, k] = 1;

s.t. make_legible{i in 1..9, j in 1..9}: sum{k in 1..9} x[i,j,k]*k = y[i,j];


/* example sudoku below (from wikipedia) */
s.t. a1: x[1,9,5]=1;
s.t. a2: x[1,8,6]=1;
s.t. a3: x[1,6,8]=1;
s.t. a4: x[1,5,4]=1;
s.t. a5: x[1,4,7]=1;
s.t. a6: x[2,9,3]=1;
s.t. a7: x[2,7,9]=1;
s.t. a8: x[2,3,6]=1;
s.t. a9: x[3,7,8]=1;
s.t. a10: x[4,8,1]=1;
s.t. a11: x[4,5,8]=1;
s.t. a12: x[4,2,4]=1;
s.t. a13: x[5,9,7]=1;
s.t. a14: x[5,8,9]=1;
s.t. a15: x[5,6,6]=1;
s.t. a16: x[5,4,2]=1;
s.t. a17: x[5,2,1]=1;
s.t. a18: x[5,1,8]=1;
s.t. a19: x[6,8,5]=1;
s.t. a20: x[6,5,3]=1;
s.t. a21: x[6,2,9]=1;
s.t. a22: x[7,3,2]=1;
s.t. a23: x[8,7,6]=1;
s.t. a24: x[8,3,8]=1;
s.t. a25: x[8,1,7]=1;
s.t. a26: x[9,6,3]=1;
s.t. a27: x[9,5,1]=1;
s.t. a28: x[9,4,6]=1;
s.t. a29: x[9,2,5]=1;
s.t. a30: x[9,1,9]=1;
end;