param given {1..9, 1..9} integer, in 0..9;
# given[i,j] > 0 is the value given for row i, col j
# given[i,j] = 0 means no value given
var X {1..9, 1..9} integer, in 1..9;
# x[i,j] = the number assigned to the cell in row i, col j
subj to AssignGiven {i in 1..9, j in 1..9: given[i,j] > 0}:
X[i,j] = given[i,j];
# assign given values
subj to Rows {i in 1..9}:
alldiff {j in 1..9} X[i,j];
# cells in the same row must be assigned distinct numbers
subj to Cols {j in 1..9}:
alldiff {i in 1..9} X[i,j];
# cells in the same column must be assigned distinct numbers
subj to Regions {I in 1..9 by 3, J in 1..9 by 3}:
alldiff {i in I..I+2, j in J..J+2} X[i,j];
# cells in the same region must be assigned distinct numbers