需要帮助理解方程答案

【问题标题】：Need help understanding the equation需要帮助理解方程
【发布时间】：2012-09-01 19:42:48
【问题描述】：

有等式 Pell x*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]

为什么？

附：有效答案：[y = 448036604040, x = 6224323426849]

【问题讨论】：

标签： z3 z3py

【解决方案1】：

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

 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) 尝试使用n 位查找x 和y 的值。

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

话虽如此，使用位向量算术求解 Pell 方程非常昂贵。问题是乘法对于位向量求解器来说真的很难。 Z3 使用的编码复杂度是n 的二次方。在我的机器上，我只设法解决了具有小解的 Pell 方程。示例：d = 982、d = 980、d = 1000、d = 1001。在所有情况下，我都使用了小于24 的n。我认为对于具有非常大的最小正解的方程没有希望，例如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)

【讨论】：