需要帮助理解等式 [英] Need help understanding the equation

问题描述

有等式 Pell x*x - 193 * y*y = 1

在 z3py 中:

x = BitVec('x',64)y = BitVec('y',64)解决(x*x - 193 * y*y == 1，x > 0，y > 0)

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

为什么?

附言有效答案:[y = 448036604040，x = 6224323426849]

解决方案

可以使用位向量算法来求解丢番图方程.基本思想是使用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 的位数，那么它最终会被找到模数资源，例如内存和时间.使用这些函数，我们可以将佩尔方程 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

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

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

def mul(x, y):sz1 = x.sort().size()sz2 = y.sort().size()返回 ZeroExt(sz2, x) * ZeroExt(sz1, y)定义添加(x，y):sz1 = x.sort().size()sz2 = y.sort().size()rsz = 最大值(sz1, sz2) + 1返回 ZeroExt(rsz - sz1, x) + ZeroExt(rsz - sz2, y)定义方程(x，y):sz1 = x.sort().size()sz2 = y.sort().size()rsz = 最大值(sz1，sz2)返回 ZeroExt(rsz - sz1, x) == ZeroExt(rsz - sz2, y)def num_bits(n):断言(n>= 0)r = 0当 n >0:r = r + 1n = n/2如果 r == 0:返回 1返回定义值(x):返回 BitVecVal(x, num_bits(x))def pell(d, n):x = BitVec('x', n)y = BitVec('y', n)解决(eq(mul(x,x), add(val(1), mul(val(d), mul(y, y)))) , x > 0, y > 0)

Have the equation Pell x*x - 193 * y*y = 1

in z3py:

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

Result: [y = 2744248620923429728, x = 8169167793018974721]

Why?

P.S. Valid answer: [y = 448036604040, x = 6224323426849]

解决方案

It is possible to use Bit-vector arithmetic to solve Diophantine equations. The basic idea is to use ZeroExt to avoid the overflows pointed out by Pad. For example, if we are multiplying two bit-vectors x and y of size n, then we must add n zero bits to x and y to make sure that the result will not overflow. That is, we write:

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

The following set of Python functions can be used to "safely" encode any Diophantine equation D(x_1, ..., x_n) = 0 into Bit-vector arithmetic. By "safely", I mean if there is a solution that fits in the number of bits used to encode x_1, ..., x_n, then it will eventually be found modulo resources such as memory and time. Using these function, we can encode the Pell's equation x^2 - d*y^2 == 1 as eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))). The function pell(d,n) tries to find values for x and y using n bits.

The following link contains the complete example: http://rise4fun.com/Z3Py/Pehp

That being said, it is super expensive to solve Pell's equation using Bit-vector arithmetic. The problem is that multiplication is really hard for the bit-vector solver. The complexity of the encoding used by Z3 is quadratic on n. On my machine, I only managed to solve Pell's equations that have small solutions. Examples: d = 982, d = 980, d = 1000, d = 1001. In all cases, I used a n smaller than 24. I think there is no hope for equations with very big minimal positive solutions such as d = 991 where we need approximately 100 bits to encode the values of x and y. For these cases, I think a specialized solver will perform much better.

BTW, the rise4fun website has a small timeout, since it is a shared resource used to run all research prototypes in the Rise group. So, to solve non trivial Pell's equations, we need to run Z3 on our own machines.

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)

这篇关于需要帮助理解等式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！