使用 Z3 求解线性方程

Question

我有以下线性方程。m = 2 ** 31 - 1(207560540 ∗ a + b) modulo m = 956631177(956631177 ∗ a + b) modulo m = 2037688522求解这些方程的最有效方法是什么？我使用了 Z3 但它没有找到任何解决方案。我为 Z3 求解上述方程的代码是：#! /usr/bin/pythonfrom 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 等工具可能是更好的选择；