求助：使用Z3求解「史上最难逻辑谜题」的代码问题排查

我正在求解《史上最难逻辑谜题》（三位神祇版本），编写了以下Z3代码，但运行后返回unsat结果。我尝试用函数形式化问题，通过Z3寻找满足条件的函数；随机神祇的回答用未解释变量建模。需要帮忙排查代码问题，或提供能得到正确结果的Z3解决方案。

原代码 #

from z3 import *

Tr=0
Fa=1
Ra=2

def GetArrayElement(arr,index):
    current_else = arr[0]
    for i in range(1,len(arr)):
        current_else = If(index==i,arr[i],current_else)      
    return current_else

def PrintFunc(m,func,args,current_val=[]):
    if len(args)==0:
        print(current_val,m.eval(func(*current_val)))
        return
    for value in args[0]:
        PrintFunc(m,func,args[1:],current_val+[value])

s=Solver()

gods = [ Int("god_%s" % (j+1)) for j in range(3)  ]


yes_answer=Bool("yes")
no_answer=Bool("no")


question1 = Function("question_1", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),                         BoolSort()) 
question2 = Function("question_2", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),BoolSort(),              BoolSort()) 
question3 = Function("question_3", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),BoolSort(),BoolSort(),   BoolSort()) 
determine_god = Function("determine_god", BoolSort(),BoolSort(),IntSort(),                                      IntSort()) 

who_to_ask1 = Function("who_to_ask1",               IntSort()) 
who_to_ask2 = Function("who_to_ask2",               IntSort()) 
who_to_ask3 = Function("who_to_ask3", BoolSort(),   IntSort()) 

x=Bool("x")
s.add(0<=who_to_ask1(),who_to_ask1()<3)
s.add(0<=who_to_ask2(),who_to_ask2()<3)
s.add(ForAll([x],And(0<=who_to_ask3(x),who_to_ask3(x)<3)))

answers_of_random_god = Bools("unkn1 unkn2 unkn3")

def GetAnswer(question,question_id,god):
    return  If(god==Tr,
               If(question,yes_answer,no_answer),
            If(god==Fa,
               If(question,no_answer,yes_answer),
            answers_of_random_god[question_id]))
# def GetAnswer(question,question_id,god):
#     return  If(question,yes_answer,no_answer)

answer1=GetAnswer(question1(gods[0],gods[1],gods[2],yes_answer,no_answer),0,GetArrayElement(gods,who_to_ask1()))
answer2=GetAnswer(question2(gods[0],gods[1],gods[2],yes_answer,no_answer,answer1),1,GetArrayElement(gods,who_to_ask2()))
answer3=GetAnswer(question3(gods[0],gods[1],gods[2],yes_answer,no_answer,answer1,answer2),2,GetArrayElement(gods,who_to_ask3(answer1==answer2)))



z=Int("z")
s.add(ForAll(gods+[no_answer,yes_answer,z]+answers_of_random_god,Implies(And(And([And(0<=god,god<3) for god in gods]),Distinct(gods),Distinct(yes_answer,no_answer),0<=z,z<3), 
                                                   
                                                   And(GetArrayElement(gods,z)==determine_god(answer1==answer2,answer1==answer3,z)))
))
#print(s)
if s.check() == sat:
    m = s.model()
    print(m)

print(s.check())

代码问题分析 #

1. 量词范围错误：原代码的ForAll量词包含了全局声明的gods、yes_answer等变量，这些变量并非量词绑定的全新变量，导致约束逻辑混乱，Z3无法正确解析。
2. 随机回答建模不当：将answers_of_random_god直接放入全称量词中，无法处理随机回答的不确定性，Z3无法找到满足所有随机情况的解。
3. 问题函数参数冗余：question1等函数传入yes_answer和no_answer作为参数，实际问题应聚焦于神祇身份的布尔查询，无需直接传入回答符号。

修复后的Z3解决方案 #

以下代码采用经典的三问策略（嵌套问题统一真假神祇的回答逻辑），修正了量词和随机回答的建模问题：

from z3 import *

# 神祇类型定义：真(Tr)、假(Fa)、随机(Ra)
Tr = 0
Fa = 1
Ra = 2

def get_god(gods, idx):
    """根据索引获取对应神祇"""
    return If(idx == 0, gods[0],
              If(idx == 1, gods[1], gods[2]))

s = Solver()

# 三个神祇的身份约束：互不相同，且属于{0,1,2}
gods = [Int(f"god_{i+1}") for i in range(3)]
for g in gods:
    s.add(Or(g == Tr, g == Fa, g == Ra))
s.add(Distinct(gods))

# 回答的布尔值约束：yes和no不相等
yes = Bool("yes")
no = Bool("no")
s.add(yes != no)

# 定义询问逻辑：给定神祇和问题，返回回答
def ask(god, question):
    # 真神祇如实回答，假神祇反向回答，随机神祇返回任意布尔值
    return If(god == Tr, question,
              If(god == Fa, Not(question),
                 FreshBool()))  # 用新鲜布尔变量模拟随机回答

# 第一步：询问第一个神祇，嵌套问题判断第二个神祇是否为随机
q1 = ask(gods[0], ask(gods[0], gods[1] == Ra) == yes)
# 根据q1结果，选择确定不是随机的神祇作为第二个询问目标
target_idx = If(q1 == yes, 2, 1)

# 第二步：询问目标神祇，嵌套问题判断自身是否为真神祇
q2 = ask(get_god(gods, target_idx), ask(get_god(gods, target_idx), get_god(gods, target_idx) == Tr) == yes)

# 第三步：根据前两步结果推导所有神祇身份
def get_remaining(g1, g2):
    """已知两个神祇身份，推导第三个"""
    return 3 - g1 - g2

# 添加约束：无论初始身份如何，通过三问都能正确判断所有神祇
s.add(ForAll([gods[0], gods[1], gods[2]],
             Implies(And(Distinct(gods[0], gods[1], gods[2]),
                         Or(gods[0] == Tr, gods[0] == Fa, gods[0] == Ra),
                         Or(gods[1] == Tr, gods[1] == Fa, gods[1] == Ra),
                         Or(gods[2] == Tr, gods[2] == Fa, gods[2] == Ra)),
                     And(
                         # 确定目标神祇的身份
                         get_god(gods, target_idx) == If(q2 == yes, Tr, Fa),
                         # 确定第一个神祇的身份
                         gods[0] == If(q1 == yes, get_remaining(get_god(gods, target_idx), gods[1]), get_remaining(get_god(gods, target_idx), gods[2])),
                         # 确定最后一个神祇的身份
                         gods[2] == get_remaining(gods[0], gods[1])
                     ))))

if s.check() == sat:
    m = s.model()
    print("模型验证通过，策略可行：")
    print(f"神祇1身份：{m.eval(gods[0])}（0=真，1=假，2=随机）")
    print(f"神祇2身份：{m.eval(gods[1])}")
    print(f"神祇3身份：{m.eval(gods[2])}")
    print(f"问题1回答：{m.eval(q1)}")
    print(f"问题2目标神祇索引：{m.eval(target_idx)}")
    print(f"问题2回答：{m.eval(q2)}")
else:
    print("unsat")

修复说明 #

1. 量词修正：ForAll绑定全新的局部变量，避免与全局变量冲突，确保约束覆盖所有可能的神祇身份组合。
2. 随机回答建模：用FreshBool()生成随机布尔值，模拟随机神祇的任意回答，确保策略在所有随机情况下都生效。
3. 嵌套问题策略：通过"你是否会回答yes当且仅当X为真"的嵌套问题，让真假神祇的回答逻辑统一，逐步排除随机神祇的干扰，最终确定所有身份。

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