需要帮助理解方程式

Question

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

为什么？

PS有效答案:[y = 448036604040,x = 6224323426849]

Answer 1

可以使用位向量算法来求解丢番图方程.基本思想是使用ZeroExt避免Pad指出的溢出.例如,如果我们将两个位向量x和y大小相乘n,那么我们必须添加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)尝试查找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.对于这些情况,我认为专业解算器会表现得更好.

BTW,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)