如何在Clingo中实现稳定婚姻？现有代码无法运行求解决

我尝试为5名男性和5名女性生成稳定婚姻（若存在婚姻外的两人互相偏好程度高于各自配偶，则婚姻不稳定），已定义双方的偏好排名数据，但编写的Clingo代码无法运行，不清楚问题出在哪。

1. 基础事实定义 #

homem(miguel).
homem(joao).
homem(pedro).
homem(marco).
homem(carlos).

mulher(maria).
mulher(paula).
mulher(carla).
mulher(cristina).
mulher(ana).

2. 偏好排名数据 #

pref(miguel,paula,5).
pref(miguel,ana,4).
pref(miguel,maria,3).
pref(miguel,carla,2).
pref(miguel,cristina,1).

pref(maria,carlos,5).
pref(maria,miguel,4).
pref(maria,marco,3).
pref(maria,joao,2).
pref(maria,pedro,1).

pref(joao,maria,5).
pref(joao,paula,4).
pref(joao,carla,3).
pref(joao,cristina,2).
pref(joao,ana,1).

pref(paula,marco,5).
pref(paula,carlos,4).
pref(paula,joao,3).
pref(paula,miguel,2).
pref(paula,pedro,1).

pref(pedro,paula,5).
pref(pedro,carla,4).
pref(pedro,ana,3).
pref(pedro,cristina,2).
pref(pedro,maria,1).

pref(carla,miguel,5).
pref(carla,marco,4).
pref(carla,joao,3).
pref(carla,pedro,2).
pref(carla,carlos,1).

pref(marco,maria,5).
pref(marco,carla,4).
pref(marco,paula,3).
pref(marco,cristina,2).
pref(marco,ana,1).

pref(cristina,pedro,5).
pref(cristina,joao,4).
pref(cristina,marco,3).
pref(cristina,miguel,2).
pref(cristina,carlos,1).

pref(carlos,ana,5).
pref(carlos,carla,4).
pref(carlos,paula,3).
pref(carlos,maria,2).
pref(carlos,cristina,1).

pref(ana,marco,5).
pref(ana,joao,4).
pref(ana,pedro,3).
pref(ana,carlos,2).
pref(ana,miguel,1).

3. 存在问题的实现代码 #

casamento(1..5). 

% every person belongs to one group only. 
1{in(H,M): casamento(C)}1 :- homem(H), mulher(M).

:- homem(H1), mulher(M1), homem(H2), mulher(M2), 
      pref(H1,M2,P1),pref(H1,M1,P2), P1>P2,
      pref(M2,H1,P3), pref(M2,H2,P4); P3>P4.

代码问题分析与修正方案 #

问题1：婚姻配对规则逻辑错误

原规则1{in(H,M): casamento(C)}1 :- homem(H), mulher(M).完全不符合一对一配对要求：

• casamento(C)和in(H,M)无关联，属于无效绑定
• 规则会强制每个男性和每个女性都进入某个婚姻组，导致多对多的错误配对

正确的一对一配对规则：

% 每个男性恰好匹配一名女性
1{casamento(H,M) : mulher(M)}1 :- homem(H).
% 每个女性恰好匹配一名男性
1{casamento(H,M) : homem(H)}1 :- mulher(M).

问题2：不稳定婚姻（阻塞对）规则错误

原规则存在两个关键错误：

• 误用分号;代替逻辑与,，导致只要满足单个条件就触发约束，不符合阻塞对的定义（需男女双方都互相偏好对方甚于当前配偶）
• 未约束H1-M1、H2-M2是当前配偶关系，规则会无差别检查所有男女组合

正确的禁止阻塞对规则：

:- casamento(H1,M1), casamento(H2,M2), H1!=H2, M1!=M2,
   pref(H1,M2,P1), pref(H1,M1,P2), P1>P2,
   pref(M2,H1,P3), pref(M2,H2,P4), P3>P4.

问题3：无用定义

原代码中casamento(1..5)无实际作用，可直接删除。

修正后的完整可运行代码 #

homem(miguel).
homem(joao).
homem(pedro).
homem(marco).
homem(carlos).

mulher(maria).
mulher(paula).
mulher(carla).
mulher(cristina).
mulher(ana).

pref(miguel,paula,5).
pref(miguel,ana,4).
pref(miguel,maria,3).
pref(miguel,carla,2).
pref(miguel,cristina,1).

pref(maria,carlos,5).
pref(maria,miguel,4).
pref(maria,marco,3).
pref(maria,joao,2).
pref(maria,pedro,1).

pref(joao,maria,5).
pref(joao,paula,4).
pref(joao,carla,3).
pref(joao,cristina,2).
pref(joao,ana,1).

pref(paula,marco,5).
pref(paula,carlos,4).
pref(paula,joao,3).
pref(paula,miguel,2).
pref(paula,pedro,1).

pref(pedro,paula,5).
pref(pedro,carla,4).
pref(pedro,ana,3).
pref(pedro,cristina,2).
pref(pedro,maria,1).

pref(carla,miguel,5).
pref(carla,marco,4).
pref(carla,joao,3).
pref(carla,pedro,2).
pref(carla,carlos,1).

pref(marco,maria,5).
pref(marco,carla,4).
pref(marco,paula,3).
pref(marco,cristina,2).
pref(marco,ana,1).

pref(cristina,pedro,5).
pref(cristina,joao,4).
pref(cristina,marco,3).
pref(cristina,miguel,2).
pref(cristina,carlos,1).

pref(carlos,ana,5).
pref(carlos,carla,4).
pref(carlos,paula,3).
pref(carlos,maria,2).
pref(carlos,cristina,1).

pref(ana,marco,5).
pref(ana,joao,4).
pref(ana,pedro,3).
pref(ana,carlos,2).
pref(ana,miguel,1).

% 一对一婚姻配对约束
1{casamento(H,M) : mulher(M)}1 :- homem(H).
1{casamento(H,M) : homem(H)}1 :- mulher(M).

% 禁止出现阻塞对（不稳定婚姻）
:- casamento(H1,M1), casamento(H2,M2), H1!=H2, M1!=M2,
   pref(H1,M2,P1), pref(H1,M1,P2), P1>P2,
   pref(M2,H1,P3), pref(M2,H2,P4), P3>P4.

内容的提问来源于stack exchange，提问作者João Oliveira