需要帮助理解方程

有方程佩尔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]

为什么？

P.S.有效答案：[y = 448036604040，x = 6224323426849]

来源

2012-09-07 Sergey Fe

可以使用位向量算法来求解丢番图方程组。基本思想是使用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)尝试使用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() 
    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)

来源

2012-09-08 02:48:37

需要帮助理解方程

回答

相关问题