用Prolog求解逻辑谜题得到错误结果，请求排查代码问题

问题背景 #

现有一逻辑谜题：Zod和Jenk两人，每人要么是Truthful（始终说真话），要么是Lying（始终说假话）。Zod称："我们俩都是Truthful"；Jenk称："我们中至少有一人是Lying"。正确解法为Zod是Lying，Jenk是Truthful。

我尝试用Prolog编写代码求解，但运行后得出“两人都是Truthful”的错误结论。若注释掉代码中的state(zod, truthful)，仅保留Zod为lying的选项，结果正确。以下是我的代码：

% Define the possible states for each person
state(zod, truthful).
state(zod, lying).
state(jenk, truthful).
state(jenk, lying).

% Zod says: "We are both truthful".
zod_statement :- state(zod, truthful), state(jenk, truthful).

% Jenk says: "At least one of us is lying".
jenk_statement :- state(zod, lying); state(jenk, lying).

% Check if a person's statement is true based on their state
statement(zod) :- 
    state(zod, truthful), zod_statement;
    state(zod, lying), \+ zod_statement.

statement(jenk) :- 
    state(jenk, truthful), jenk_statement;
    state(jenk, lying), \+ jenk_statement.

% The solution must satisfy both statements
solution(ZodState, JenkState) :- 
    state(zod, ZodState),
    state(jenk, JenkState),
    statement(zod),
    statement(jenk).

请问我的代码存在什么问题？

问题根源 #

你的代码核心错误在于**state/2谓词的定义方式破坏了状态的唯一性**：你把state(zod, truthful)、state(zod, lying)等都设为全局事实，这意味着Prolog会同时认可Zod既可以是truthful也可以是lying。在回溯验证statement(jenk)时，它会无视当前已经选定的ZodState = truthful，转而调用全局的state(zod, lying)事实，让jenk_statement错误成立，最终导致错误的解被输出。

举个具体的错误路径：
当程序尝试ZodState = truthful、JenkState = truthful的组合时：

1. 验证statement(zod)：因为Zod是truthful，检查zod_statement——依赖全局的state(zod, truthful)和state(jenk, truthful)，条件成立，所以statement(zod)为真。
2. 验证statement(jenk)：Jenk是truthful，需要jenk_statement为真。此时本应因为两人都是truthful而不满足，但Prolog会回溯查找state/2的其他事实，找到state(zod, lying)，使得jenk_statement成立，最终错误判定这个组合符合要求。

修复方案 #

要解决问题，必须确保每个人的状态是唯一确定的，不能同时存在两种矛盾的全局事实。推荐采用以下清晰的写法：

% 定义单个个体的可能状态
possible_state(truthful).
possible_state(lying).

% Zod陈述的逻辑：两人都是truthful
zod_claim(ZodS, JenkS) :- ZodS = truthful, JenkS = truthful.

% Jenk陈述的逻辑：至少一人是lying
jenk_claim(ZodS, JenkS) :- ZodS = lying; JenkS = lying.

% 验证陈述是否符合身份规则
valid(PersonState, Claim) :-
    PersonState = truthful, Claim;  % 说真话的人，陈述必须为真
    PersonState = lying, \+ Claim.  % 说假话的人，陈述必须为假

% 求解：为两人分配唯一状态，且陈述都符合规则
solution(ZodState, JenkState) :-
    possible_state(ZodState),
    possible_state(JenkState),
    valid(ZodState, zod_claim(ZodState, JenkState)),
    valid(JenkState, jenk_claim(ZodState, JenkState)).

修复后运行solution(Z, J).，会得到唯一正确的结果：

Z = lying, J = truthful.

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