How can I generate a graph by constraining it to be subisomorphic to a given graph, while not subisomorphic to another?

It is probably good to note that MiniZinc's limitation is not coincidental. When the creation of a free variable is negated, rather then finding a valid assignment for the variable, instead the model would have to prove that no such valid assignment exists. This is a much harder problem that would bring MiniZinc into the field of quantified constraint programming. The only general solution (to still receive the same flattened constraint model) would be to iterate over all possible values for each variable and enforce the negated constraints. Since the number of possibilities quickly explodes and the chance of getting a good model is small, MiniZinc does not do this automatically and throws this error instead.

This technique would work in your case as well. In the not_matches version of your predicate, you can iterate over all possible permutations (the possible mappings) and enforce that they not correct (partial) mappings. This would be a correct way to enforce the constraint, but would quickly explode. I believe, however, that there is a different way to enforce this constraint that will work better.

My idea stems from the fact that, although the most natural way to describe a permutation from one array to the another is to actually create the assignment from the first to the second, when dealing with discrete variables, you can instead enforce that each has the exact same number of each possible value. As such a predicate that enforces X is a permutation of Y might be written as:

predicate is_perm(array[int] of var $$E: X, array[int] of var $$E: Y) =
    let {
        array[int] of int: vals = [i | i in (dom_array(X) union dom_array(Y))]
    } in global_cardinality(X, vals) = global_cardinality(Y, vals);

Notably this predicate can be negated because it doesn't contain any free variables. All new variables (the resulting values of global_cardinality) are functionally defined. When negated, only the relation = has to be changed to !=.

In your model, we are not just considering full permutations, but rather partial permutations, and we use a dummy value otherwise. As such, the p predicate might also be written:

predicate p(array [int] of var 0..10: X, array [int] of var 1..10: Y) =
    let {
        set of int: vals = lb_array(Y)..ub_array(Y); % must not include dummy value
        array[vals] of var int: countY = global_cardinality(Y, [i | i in vals]);
        array[vals] of var int: countX = global_cardinality(X, [i | i in vals]);
    } in forall(i in vals) (countX[i] <= countY[i]);

Again this predicate does not contain any free variables, and can be negated. In this case, the forall can be changed into a exist with a negated body.

There are a few things that we can still do to optimise p for this use case. First, it seems that global_cardinality is only defined for variables, but since Y is guaranteed par, we can rewrite it and have the correct counts during MiniZinc's compilation. Second, it can be seen that lb_array(Y)..ub_array(Y) gives the tighest possible set. In your example, this means that only slightly different versions of the global cardinality function are evaluated, that could have been

predicate p(array [1..5] of var 0..10: X, array [1..5] of 1..10: Y) =
let {
    % CHANGE: Use declared values of Y to ensure CSE will reuse `global_cardinality` result values.
    set of int: vals = 1..10; % do not include dummy value
    % CHANGE: parameter evaluation of global_cardinality
    array[vals] of int: countY = [count(j in index_set(Y)) (i = Y[j]) | i in vals];
    array[vals] of var int: countX = global_cardinality(X, [i | i in 1..10]);
} in forall(i in vals) (countX[i] <= countY[i]);

Regarding the example. One approach might be to rewrite the not p(...) constraint to a specific not_p(...) constraint. But I'm how sure how that be formulated.

Here's an example but it's probably not correct:

predicate not_p(array [1..5] of var 0..10:arr1, array [1..5] of 1..10:arr2)=
  let{
  array [1..5] of var 1..5: mapping;
        constraint all_different(mapping)
  } in
  exists(i in 1..5)(
    arr1[i] != 0
    /\
    arr1[i] != arr2[mapping[i]]
   
);

This give 500 solutions such as

arr = [1, 0, 0, 0, 0];
----------
arr = [2, 0, 0, 0, 0];
----------
arr = [3, 0, 0, 0, 0];
...
----------
arr = [2, 0, 0, 3, 4];
----------
arr = [2, 0, 1, 3, 4];
----------
arr = [2, 1, 0, 3, 4];

Update I added not before the exists loop.