MiniZinc实现正负子图同构约束模式图的技术问询

简述：如何生成满足如下约束的图模式：对正例列表内所有图满足子图同构匹配，对负例列表内所有图均不满足子图同构匹配？
现有一批标注为正/负类的有向异构属性图，需要找到规模最小的带特殊取值的图模式集合，满足如下规则：

1. 每个输入图都存在可匹配的模式（匹配定义：模式P子图同构于图G，且映射节点的属性值完全一致）
2. 正类模式仅可匹配正例图
3. 正类模式不可匹配任何负例图
4. 负类模式仅可匹配负例图
5. 负类模式不可匹配任何正例图（注：原文此处笔误写为“不可匹配任何负例图”，与上一条规则逻辑冲突）

示例说明 #

输入：g1(+),g2(-),g3(+),g4(+),g5(-),g6(+)

• 可接受解：p1(+),p2(+),p3(-)，其中p1(+)匹配g1(+)、g4(+)；p2(+)匹配g3(+)、g6(+)；p3(-)匹配g2(-)、g5(-)
• 不可接受解：p1(+),p2(-)，其中p1(+)匹配g1(+),g2(-),g3(+)；p2(-)匹配g4(+),g5(-),g6(+)

当前问题 #

目前已实现生成可匹配列表内所有图的逻辑，但无法落地“正类模式不匹配任何负例图”的约束：编写了输入为模式、图的matches谓词，通过局部变量数组mapping尝试完成节点映射，但在否定上下文调用该谓词时，返回错误：MiniZinc: flattening error: free variable in non-positive context。
尝试编写反向谓词not_matches，但尚未找到正确方式表述“对所有可能的节点映射，子图同构关系均不成立”的逻辑；同时无法将mapping变量定义在谓词外部，因为单个模式可多次匹配同一图，需要获取所有合法映射关系。

可复现代码 #

include "globals.mzn";

predicate 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 (forall(i in 1..5)(arr1[i]=0\/arr1[i]=arr2[mapping[i]]));


array [1..5] of var 0..10:arr;
constraint p(arr,[1,2,3,4,5]);
constraint  p(arr,[1,2,3,4,6]);
constraint  not p(arr,[1,2,3,5,6]);

solve satisfy;

针对该示例：决策变量为数组，谓词p为真当且仅当存在合法映射可完成数组值的匹配，数组中元素可取值0作为通配符：

• [1,2,3,4,0]为合法解
• [0,0,0,0,0]为非法解：它可匹配任意数组，不符合“不可匹配[1,2,3,5,6]”的约束
• [1,2,3,4,7]为非法解：它无法匹配任何输入参数数组（参数数组中不存在取值7）

报错的核心原因是MiniZinc不支持在非正（否定）上下文里处理带存在量词的局部自由变量。原谓词里的mapping是存在量词限定的局部变量，直接对谓词取反时，求解器无法自动完成从存在量词到全称量词的扁平化转换，就会抛出上述错误。

不要直接对带局部存在变量的谓词取反，分开实现正向匹配、反向不匹配两个独立谓词即可：

1. 正向matches谓词保留原有逻辑：存在一个合法节点映射，满足子图同构+属性匹配要求，用来约束模式必须覆盖对应类别的所有样本
2. 反向not_matches谓词显式枚举所有合法的节点映射，约束所有映射都不满足匹配要求，用来限制模式不能匹配异类样本

针对给出的简化示例，修正后的可运行代码如下：

include "globals.mzn";

% 正向匹配谓词：存在合法映射满足匹配规则
predicate matches(array [1..5] of var 0..10:pattern, array [1..5] of 1..10:target) =
    let {
        array [1..5] of var 1..5: mapping;
        constraint all_different(mapping);
    } in forall(i in 1..5)(pattern[i] = 0 \/ pattern[i] = target[mapping[i]]);

% 反向不匹配谓词：所有合法映射均不满足匹配规则
predicate not_matches(array [1..5] of var 0..10:pattern, array [1..5] of 1..10:target) =
    forall(mapping in permutations(1..5))(
        exists(i in 1..5)(pattern[i] != 0 /\ pattern[i] != target[mapping[i]])
    );

array [1..5] of var 0..10:arr;
% 正向约束：必须匹配两个正例数组
constraint matches(arr, [1,2,3,4,5]);
constraint matches(arr, [1,2,3,4,6]);
% 反向约束：必须不匹配负例数组
constraint not_matches(arr, [1,2,3,5,6]);
% 剪枝约束：非通配符取值必须在正例中存在，避免出现7这类无效值
constraint forall(i in 1..5)(arr[i] = 0 \/ arr[i] in {1,2,3,4,5,6});

solve satisfy;

代码里用permutations(1..5)直接枚举所有长度为5的合法排列（即所有满足双射要求的节点映射），不需要在谓词内部定义局部自由变量，从根源上规避了非正上下文的变量错误。

迁移到实际的图挖掘场景时，只需要把排列枚举逻辑替换成符合子图同构要求的合法节点映射枚举即可：如果图规模较大，全枚举性能差，可以提前按节点属性、边连接关系做剪枝，过滤掉不可能成立的映射，不需要枚举所有理论上的排列。

内容的提问来源于stack exchange，提问作者Julien Carayol