需要幫助理解方程

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

需要幫助理解方程

回答

相關問題