有没有大佬喜欢逻辑分析的，来玩玩这题

[quote][tid=30008636]Topic[/tid] Post by [uid=63728098]WhenMoving[/uid] (2021-12-26 04:53):

如图
[img]https://img.nga.178.com/attachments/mon_202112/26/-7Q2p-gzedZbT1kSg0-sg.jpg.medium.jpg[/img][/quote]连线题[s:ac:茶]

[quote][tid=30008636]Topic[/tid] Post by [uid=63728098]WhenMoving[/uid] (2021-12-26 04:53):

如图
[img]https://img.nga.178.com/attachments/mon_202112/26/-7Q2p-gzedZbT1kSg0-sg.jpg.medium.jpg[/img][/quote]1亚瑟夫 唱歌
2英国 律师
3澳大利亚 作曲 医生或农场主
4巴顿 非医生
5德国 霍夫 非农场主非律师
6农场主 跳舞

希尔 澳大利亚 作曲 医生
霍夫 德国 弹钢琴 售货员
亚瑟夫 英国 唱歌 律师
巴顿 加拿大 跳舞 农场主

[quote][pid=576462410,30008636,1]Reply[/pid] Post by [uid=39469877]沈梦遥[/uid] (2021-12-26 05:07):

1亚瑟夫 唱歌
2英国 律师
3澳大利亚 作曲 医生或农场主
4巴顿 律师或售货员或红场主
5德国 霍夫 医生或售货员
6农场主 跳舞

36得 澳大利亚 作曲 医生 再由145知此人只能为希尔
故得
7希尔 澳大利亚 作曲 医生
由57知霍夫只能为售货员
再由167知爱好只能为弹钢琴
故得
8霍夫 德国 弹钢琴 售货员
由78亚瑟夫只能为农场主或律师 由6知非农场主
故得
9亚瑟夫 英国 唱歌 律师
最后
巴顿 加拿大 跳舞 农场主

这种问题应该能用形式化验证语言求解[/quote]看起来好像可以量化后用z3解