enum COLOR;
int: width; int: height;
set of int: WIDTH = 1..width;
set of int: HEIGHT = 1..height;
array[HEIGHT, WIDTH] of COLOR: init;
array[HEIGHT, WIDTH] of var COLOR: board;

predicate n_neighbor(var int: i, var int: j, int: count) =
    let { var COLOR: c  = board[i, j] } in
    sum([
        if i > 1 then c == board[i-1, j] else false endif,
        if i < height then c == board[i+1, j] else false endif,
        if j > 1 then c == board[i, j-1] else false endif,
        if j < width then c == board[i, j+1] else false endif
    ]) == count;

constraint forall(i in HEIGHT, j in WIDTH)(
    if init[i, j] != X then
        % X is blank
        board[i, j] = init[i, j] /\ n_neighbor(i, j, 1)
    else
        n_neighbor(i, j, 2)
    endif
);

solve satisfy;