1 4
0 2 5 7
  3 6

5 3
2 8 1 7
  6 4

2 6
0 3 7 10
1 4 8 11
  5 9

include "globals.mzn";

int: rows;
int: cols;
int: n = sum(i in 1..rows, j in 1..cols) ( bool2int(mat[i,j] > 0) );
array[1..rows, 1..cols] of int: mat;

array[1..n] of var 1..n: x; % decision variables

solve satisfy;

constraint
  all_different(x)
  /
  % constrain all the neighbours for each cell
  forall(i in 1..rows, j in 1..cols where mat[i,j] > 0) (
     forall(a,b in {-1,0,1} where
            i+a >= 1    / j+b >=  1   /
            i+a <= rows / j+b <= cols /
            not(a = 0 / b = 0)        /
            mat[i+a,j+b] > 0
         )
           (  % the constraints
              abs(x[mat[i,j]] - x[mat[i+a,j+b]])>1
           )
   )
;

output [ show(x) ];

% Problem 2: 12 sized
rows = 4;
cols = 4;

% 0 means empty cell
mat = array2d(1..rows, 1..cols,
[
 0, 3,  7,  0,
 1, 4,  8, 11,
 2, 5,  9, 12,
 0, 6, 10,  0
]);

import java.util.*;

public class NumberCrossPuzzle
{
    public static void main(String[] args)
    {
        int w = 4, h = 4, m = 1, n = 1;

        Map<State, Long> freq = new HashMap<State, Long>();
        freq.put(State.initialState(w, h, m, n), 1L);

        int squares = w * h - 4 * m * n;
        for (int i = 0; i < squares; i++) {
            Map<State, Long> nextFreq = new HashMap<State, Long>();
            for (Map.Entry<State, Long> e : freq.entrySet()) {
                for (State succ : e.getKey().successors(w, h)) {
                    Long l = nextFreq.get(succ);
                    if (l == null) l = 0L;
                    if (l < 0L) throw new IllegalStateException("Overflow detected");
                    nextFreq.put(succ, l + e.getValue());
                }
            }
            freq = nextFreq;
        }

        Long total = 0L;
        for (Long l : freq.values()) {
            if (l < 0L) throw new IllegalStateException("Overflow detected");
            total += l;
            if (total < 0L) throw new IllegalStateException("Overflow detected");
        }
        System.out.println(total);
    }

    private static class State
    {
        private final int mask, x, y;

        private State(int mask, int x, int y) {
            this.mask = mask;
            this.x = x;
            this.y = y;
        }

        static State initialState(int w, int h, int m, int n) {
            if (w * h > 32) throw new IllegalArgumentException("Need a larger mask");
            if (m * 2 >= w) throw new IllegalArgumentException("Corner holes too wide");
            if (n * 2 >= h) throw new IllegalArgumentException("Corner holes too high");

            int mask = 0;
            for (int y = 0; y < n; y++) {
                for (int x = 0; x < m; x++) {
                    // TL, TR, BL, BR
                    mask ^= 1 << (y * w + x);
                    mask ^= 1 << ((w - 1 - y) * w + x);
                    mask ^= 1 << (y * w + (h - 1 - x));
                    mask ^= 1 << ((w - 1 - y) * w + (h - 1 - x));
                }
            }

            return new State(mask, -1, -1);
        }

        Iterable<State> successors(int w, int h) {
            List<State> rv = new ArrayList<State>();
            for (int j = 0; j < h; j++) {
                for (int i = 0; i < w; i++) {
                    int bit = 1 << (j * w + i);
                    if ((mask & bit) != 0) continue;
                    if ((x - i) * (x - i) + (y - j) * (y - j) <= 2) continue;
                    rv.add(new State(mask | bit, i, j));
                }
            }
            return rv;
        }

        @Override
        public int hashCode() {
            return (mask * 37 + x) * 37 + y;
        }

        @Override
        public boolean equals(Object obj) {
            if (!(obj instanceof State)) return false;
            State s = (State)obj;
            return s.mask == mask && s.x == x && s.y == y;
        }
    }
}