使用 Z3 求解线性方程

Question

我有以下线性方程。

m = 2 ** 31 - 1

(207560540 ∗ a + b) modulo m = 956631177

(956631177 ∗ a + b) modulo m = 2037688522

求解这些方程的最有效方法是什么？

我使用了 Z3 但它没有找到任何解决方案。我为 Z3 求解上述方程的代码是：

#! /usr/bin/python

from z3 import *

a = Int('a')

b = Int('b')

s = Solver()

s.add((a * 207560540 + b) % 2147483647 == 956631177)

s.add((a * 956631177 + b) % 2147483647 == 2037688522)

print s.check()

print s.model()

我知道答案是：a = 16807, b = 78125，但是，我怎样才能让 Z3 解决它呢？

我尝试的另一种方法是将 a 和 b 设置为 BitVec() 而不是 Integers ，如下所示：

a = BitVec('a', 32)

b = BitVec('b', 32)

这给了我一个不正确的解决方案，如下所示：

[b = 3637638538, a = 4177905984]

有没有办法用Z3解决它？

Answer 1

顺便说一句关于位向量：当您使用位向量，则所有操作完成模2^N哪里N是位向量的大小。所以， z3 没有给你一个incorrect解决方案：如果你做数学 modulo 2^32，你会发现它找到的模型确实是正确的。看来您的问题确实需要无界整数，并且由于模数并不是真正的线性2^31-1。（线性意味着乘以常数；常数乘以模数带您进入不同的领域。）而模数并不容易推理；我认为 z3 不是解决此类问题的正确工具，也不是任何其他 SMT 求解器。在这种情况下，像 mathematica、wolfram-alpha 等工具可能是更好的选择；