z3 - 需要帮助理解方程

Question

有方程 Pellx*x - 193 * y*y = 1

在 z3py 中：

x = BitVec('x',64)
y = BitVec('y',64)
solve(x*x - 193 * y*y == 1, x > 0, y > 0)

结果：[y = 2744248620923429728, x = 8169167793018974721]

为什么？

PS 有效答案：[y = 448036604040，x = 6224323426849]

Answer 1

可以使用位向量算术来求解丢番图方程。基本思想是用来ZeroExt避免Pad指出的溢出。例如，如果我们将两个位向量乘以size x，那么我们必须将零位添加到and以确保结果不会溢出。也就是说，我们写：ynnxy

 ZeroExt(n, x) * ZeroExt(n, y)

以下 Python 函数集可用于“安全地”将任何丢番图方程编码D(x_1, ..., x_n) = 0为位向量算术。通过“安全”，我的意思是如果有适合用于编码的位数的解决方案x_1, ..., x_n，那么最终将找到模资源，例如内存和时间。使用这些函数，我们可以将 Pell 方程编码x^2 - d*y^2 == 1为eq(mul(x, x), add(val(1), mul(val(d), mul(y, y))))。该函数pell(d,n)尝试查找x和y使用n位的值。

以下链接包含完整示例： http ://rise4fun.com/Z3Py/Pehp

话虽如此，使用位向量算术求解 Pell 方程是非常昂贵的。问题是乘法对于位向量求解器来说真的很难。Z3 使用的编码复杂度是 上的二次方n。在我的机器上，我只设法解决了具有小解的 Pell 方程。例子：d = 982, d = 980, d = 1000, d = 1001. 在所有情况下，我都使用了n小于24. 我认为对于具有非常大的最小正解的方程没有希望，例如d = 991我们需要大约 100 位来编码 和 的x值y。对于这些情况，我认为专门的求解器会表现得更好。

顺便说一句，rise4fun 网站的超时时间很小，因为它是一个共享资源，用于运行 Rise 组中的所有研究原型。因此，要求解非平凡的 Pell 方程，我们需要在自己的机器上运行 Z3。

def mul(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  return ZeroExt(sz2, x) * ZeroExt(sz1, y)
def add(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  rsz = max(sz1, sz2) + 1
  return ZeroExt(rsz - sz1, x) + ZeroExt(rsz - sz2, y)  
def eq(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  rsz = max(sz1, sz2)
  return ZeroExt(rsz - sz1, x) == ZeroExt(rsz - sz2, y)
def num_bits(n):
  assert(n >= 0)
  r = 0
  while n > 0:
    r = r + 1
    n = n / 2
  if r == 0:
    return 1
  return r
def val(x):
  return BitVecVal(x, num_bits(x))
def pell(d, n):
  x  = BitVec('x', n)
  y  = BitVec('y', n)
  solve(eq(mul(x,x), add(val(1), mul(val(d), mul(y, y)))) , x > 0, y > 0)