Z3 Solver::check() 卡在可解输入上

Question

在 AOC2024 的第 17 天，虚拟机出现了一个问题，其中应该通过识别输入是以 3 位块读取的方式来暴力破解输入，从而产生特定的输出（因此 //= 8） 。虽然我后来使用蛮力得到了解决方案，但我想使用不同的解决方案，因为我看到有人使用 SAT 求解器。当然，每个人的程序都不同，所以我不能只查看如何使用 SAT 求解器，但无论如何我想尝试学习如何使用 Z3。

我应该注意，我以前从未使用过Z3，所以如果我做了一些非常愚蠢的事情，那么我很抱歉，但我想学习正确的方法。

from z3 import IntVal, Int2BV, BV2Int, Solver, Int


def program(a):
    b = 0
    c = 0
    output = []

    while a > 0:
        b = a % 8
        b = b ^ 6
        denominator = 2**b
        c = a // denominator
        b = b ^ c
        b = b ^ 4
        output.append(b % 8)
        a //= 8

    return output


print(program(123))  # [ 2, 2, 3 ]
output = [2, 2, 3]

a = Int('a')

s = Solver()
s.add(a > 0)

# constants
eight = IntVal(8)

six = IntVal(6)
six_bv = Int2BV(six, 32)

four = IntVal(4)
four_bv = Int2BV(four, 32)

a_temp = a
for x in output:
    # b = a % 8
    s1 = a_temp % eight
    s1_bv = Int2BV(s1, 32)

    # b = b ^ 6
    s2_bv = s1_bv ^ six_bv
    s2 = BV2Int(s2_bv)

    # c = a / (2 ** b)
    s3_denom = IntVal(2) ** s2
    s3 = a_temp / s3_denom
    s3_bv = Int2BV(s3, 32)

    # b = b ^ c
    s4_bv = s2_bv ^ s3_bv

    # b = b ^ 4
    s5_bv = s4_bv ^ four_bv
    s5 = BV2Int(s5_bv)

    # out(b % 8)
    character = s5 % eight

    print(character, "==", x)
    s.add(character == x)
    a_temp = a_temp / 8

s.add(a_temp == 0)

print(s.check())
print(s.model())

问题最初是用自定义的ISA来表示的，所以我将其反编译并重写为python，即我在顶部定义的程序函数。 代入 123 得到 [2, 2, 3]。现在我尝试通过强制每个数字与输出相同来为 Z3 提供相同的算法。

然而，Z3 在调用 s.check() 时挂起，当提供较小的输入时，有时我会变得未知，我无法将其输出 sat 并给我曾经用于生成输出的数字。

我已经尝试使用更多/更少的方程来运行（例如，我后来添加了 a > 0 并且还添加了 a_temp 最终为 == 0，以便可以打破循环）。

我也想过Z3是否正确处理整数除法，但我的测试似乎表明Z3确实默认执行整数除法，所以它应该已经是正确的。

Answer 1

混合和匹配整数/位向量通常会导致 SMT 求解器出现性能问题，因为它们之间的转换会产生非线性约束。

非线性算术是不可判定的。而且它们使用的算法并不是特别有效。因此，您可能会得到

unknown

，或者求解器可能会永远循环，除非某些启发式命中并产生解决方案。因此，如果可以的话，在进行算术运算时应避免混合和匹配不同类型的数字。

我还没有研究原始的 AOC 问题，但我假设它允许

a

/

b

/

c

值为任意整数。所以，你确实可以用 z3 的

Int

来建模。但是您不断在 32 位位向量之间来回转换它们，因此从某种意义上说，它们无论如何都不会被处理为无界值。因此，我会明确表示：忘记无界整数，只需将

a

/

b

/

c

限制为 32 位机器整数即可。 （这是否可以接受当然取决于问题。）

基于此，我将你的问题编码如下：

from z3 import *

output = [2, 2, 3]

s = Solver()

a, b, c = BitVecs('a b c', 32)
s.add(a > 0)

for x in output:
   b = a % 8
   b = b ^ 6
   denominator = 1 << b
   c = a / denominator
   b = b ^ c
   b = b ^ 4
   s.add (x == b % 8)
   a /= 8

s.add(a <= 0)

print(s.check())
print(s.model())

当我运行这个时，我得到：

sat
[a = 115]

所以，z3 建议

a

的值应该是 115。从你的问题来看，我推测你希望这个值实际上是 123。好吧，事实证明，不同的程序可以产生相同的输出。确实：

def program(a):
    b = 0
    c = 0
    output = []

    while a > 0:
        b = a % 8
        b = b ^ 6
        denominator = 2**b
        c = a // denominator
        b = b ^ c
        b = b ^ 4
        output.append(b % 8)
        a //= 8

    return output

print(program(123))
print(program(115))

打印：

[2, 2, 3]
[2, 2, 3]

所以，看起来 z3 成功地对你的问题进行了逆向工程。它只是发现一个不同的起始状态恰好产生相同的输出。

长话短说，SMT 求解器确实适合此类逆向工程问题，但也有局限性。尝试尽可能坚持使用位向量，特别是如果可以的话，不要混合搭配不同类型的数字。