为何Z3无法自动求解存在平凡解的PRNG位向量约束问题

运行下方代码时，前3次solve调用都能正常返回结果，执行到最后一行solve(safePrngDut,justCheck=False)时会永久阻塞无响应：

• 传入justCheck=True时，Z3只需要校验a=b=0是否满足约束，可以瞬间完成验证
• 从逻辑上人脑可以直接判定a=b=0是合法解：代码里所有运算都是异或、循环移位、模2^64加法、按位与操作，初始状态全0时，后续所有状态、运算输出都会保持为0，完全符合输出为0的要求
• 这个问题的逻辑复杂度远低于SHA2原像求解类密码难题，但Z3跑几个小时也没法自己找到这个解。

from z3 import *
import sys
bit64 = 0xffffffffffffffff

desiredOut1=0
desiredOut2=0

def rotl64(x, shift):
    return ((x << shift) | LShR(x, 64 - shift))  & bit64

def prng(state):
    a = state[0]
    b = state[1]
    axorb = a ^ b
    newa, newb = (rotl64(a,55) ^ axorb ^ (axorb << 14)) & bit64, rotl64(axorb,36)
    return [newa,newb],(a+b) & bit64

def prngAcc(state,n):
    assert(n>0)
    state,out = prng(state)
    for i in range(0,n-1):
        state,o= prng(state)
        out ^= o
    return state,out

def refreshEntropyPool(state,n):
    state,el = prngAcc(state,n)
    state,eh = prngAcc(state,n)
    state[0] ^= el 
    state[1] ^= eh
    assert(len(state)==2)
    state.append(el)
    state.append(eh)
    return state 

def safePrng(state,n):
    if len(state)> 2:
        # 注入熵池
        state[0] ^= state[2] 
        state[1] ^= state[3]
    else:
        # 初始化熵池
        state.append(state[0]^state[0]) # 生成和state[0]同类型的0值
        state.append(state[1]^state[1]) # 生成和state[1]同类型的0值
    print(state)
    state = refreshEntropyPool(state,n)
    tmp,out = prng(state)
    state[0] = tmp[0]
    state[1] = tmp[1]
    return state,out

def safePrngDut(state):
    return safePrng(state,1)

def solve(dut, justCheck):
    a, b = BitVec('a', 64), BitVec('b', 64)
    s = Solver()
    initState = [a,b]
    state1,out1 = dut(initState)
    state2,out2 = dut(state1)
    s.add(out1 == desiredOut1,out2 == desiredOut2)
    if justCheck:
        s.add(a == 0, b==0)
    s.check()
    m = s.model()
    print("%s %s"%(hex(m[a].as_long()).upper(), hex(m[b].as_long()).upper()))

solve(prng,justCheck=True)
solve(prng,justCheck=False)
solve(safePrngDut,justCheck=True)
print("Z3 rocks so far")
solve(safePrngDut,justCheck=False) # 该行会永久阻塞

卡壳和问题本身的逻辑复杂度没有关系，不是问题难到算不出来，是Z3位向量求解器的工作逻辑和公式结构共同导致的：

• Z3不会优先搜索人类眼里的“简单解”
  处理64位位向量约束时，Z3默认会把所有运算拆成布尔逻辑门，转成SAT问题用CDCL算法求解。这个算法的搜索顺序靠内置的分支启发式规则决定，从来不会按照“数值从小到大”的顺序枚举可能的答案，更不会主动识别“全0是状态不动点”这类高层逻辑特征。全0解虽然人一眼就能看出来，但在求解器的搜索顺序里优先级极低，很可能绕几个小时都碰不到这个赋值。
• 多轮运算嵌套导致布尔公式规模膨胀
  每轮prng调用包含1次64位模2^64加法，这类带进位传播的运算属于位向量上的非线性操作，会把每个低位的约束传递到所有高位，再和循环移位、异或、左移操作嵌套6次（两次safePrng调用总共执行6次prng）之后，整个约束展开成布尔CNF子句会产生上万条规则，每个比特的取值都和其他几十个比特存在依赖关系，搜索时冲突推导的开销会变得非常高。
• 校验解和求解解的复杂度存在数量级差距
  当添加a=0、b=0的约束后，Z3不需要做任何搜索，直接通过常量传播把所有中间表达式折叠成常量0，瞬间就能验证约束成立，这个过程和无引导遍历整个2^128大小的搜索空间相比，计算量差了十几个数量级。

想让Z3快速找到解非常简单，要么给求解器配置位向量专用的快速求解策略，要么手动引导搜索顺序即可，比如在调用s.check()前替换默认求解器为位向量优化的策略链，就可以在毫秒级得到a=0、b=0的结果：

# 替换默认求解器为位向量优化的求解策略
s = Then('simplify', 'solve-eqs', 'bit-blast', 'sat').solver()

哪怕手动先试探a=0的场景，也能瞬间算出b=0的合法解，不会出现长时间阻塞的问题。

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