为何Alloy 4无法为10人规模的Halmos握手问题模型找到实例？

我尝试用Alloy 4解决Halmos握手问题（第2.3节），因课程要求必须使用Alloy 4，这是练习而非作业。我构建了如下模型：

module halmos

abstract sig Person { shook : set Person }
sig Man extends Person { wife : one Woman }
sig Woman extends Person { husband : one Man }
one sig Me in Man { }
one sig MyWife in Woman { }

fact {
    Me.wife = MyWife
    MyWife.husband = Me
}

// hand-shaking is symmetric
fact { all p : Person | p.shook = shook.p }

// "No one shook his or her own hand"
fact { all p : Person | p not in p.shook }

// "no husband shook his wife’s hand"
// this and symmetricity of shook implies no wife shook her husband's hand
fact { all m : Man | m.wife not in m.shook }

fact monogamy {
    all m : Man, w : Woman |
        // these parens are needed for correct precedence
        (m.wife = w implies w.husband = m)
        and
        (w.husband = m implies m.wife = w)
}

// all distinct persons (other than Me) shook a different number of hands
fact {
    all disj p1,p2 : Person - Me |
        #p1.shook != #p2.shook
}

按照问题描述，应该存在10个Person的符合规范的实例，但Alloy找不到。执行run { } for exactly 10 Person返回无实例，而run { } for exactly 8 Person和run { } for exactly 4 Person能成功找到实例，run { } for exactly 5 Person因人数为偶数要求失败，符合预期。请问是Alloy使用错误还是模型规范存在问题？

问题根源：模型遗漏核心约束 #

你的模型存在两个关键问题：

1. 未明确所有参会者都是夫妻，无单身者：Halmos握手问题的前提是所有参会者都是成对的夫妻，你没有约束Man和Woman的数量相等，也没限定Person只能是Man或Woman的并集。当指定10个Person时，Alloy可能生成数量不等的男女（比如6男4女），这直接违反问题的隐含前提。
2. 一夫一妻约束冗余且不够严谨：原monogamy事实的写法繁琐，用关系逆操作可以更准确表达夫妻关系的双向绑定。

修复方案 #

添加以下约束，并简化一夫一妻规则：

// 所有参会者都是夫妻，无单身
fact all_married {
    Person = Man + Woman
    #Man = #Woman
}

// 简化一夫一妻约束：妻子关系是丈夫关系的逆
fact monogamy {
    wife = ~husband
}

修改后，执行run { } for exactly 10 Person就能找到符合要求的实例了。本质是你之前的模型没有限定男女数量对等，导致10人场景下可能出现非夫妻的单身角色，破坏了握手次数的逻辑可能性。

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