Potrzebujesz pomocy zrozumienie równanie

Question

Czy równanie Pell x*x - 193 * y*y = 1

w z3py:

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

Wynik: [y = 2744248620923429728, x = 8169167793018974721]

Dlaczego?

P.S. Prawidłowa odpowiedź: [y = 448036604040, x = 6224323426849]

Answer 1

Do rozwiązywania równań diofantycznych można zastosować arytmetykę wektorów bitowych. Podstawową ideą jest użycie ZeroExt, aby uniknąć przelewów wskazanych przez Pad. Na przykład, jeśli mnożymy dwa bitowe wektory x i y o rozmiarze n, musimy dodać n zero bitów do x i y, aby upewnić się, że wynik nie zostanie przepełniony. Oznacza to, że możemy napisać:

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

Poniższy zestaw funkcji Pythona mogą być wykorzystywane do „bezpiecznie” zakodować dowolny równanie diofantyczne D(x_1, ..., x_n) = 0 do Bit-wektor arytmetyki. Przez "bezpiecznie" rozumiem, że jeśli istnieje rozwiązanie pasujące do liczby bitów użytych do kodowania x_1, ..., x_n, to ostatecznie zostaną znalezione zasoby modulo, takie jak pamięć i czas. Korzystając z tej funkcji, możemy zakodować równanie Pella x^2 - d*y^2 == 1 jako eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))). Funkcja pell(d,n) próbuje znaleźć wartości dla x i y przy użyciu bitów n.

Poniższy link zawiera kompletny przykład: http://rise4fun.com/Z3Py/Pehp

Powiedział, że to jest super drogie, aby rozwiązać Równanie Pella korzystania Bit-wektor arytmetyki. Problem polega na tym, że mnożenie jest naprawdę trudne dla solver-wektora. Złożoność kodowania używanego przez Z3 jest kwadratowa na n. Na moim komputerze udało mi się tylko rozwiązać równania Pella, które mają małe rozwiązania. Przykłady: d = 982, d = 980, d = 1000, d = 1001. We wszystkich przypadkach użyłem numeru n mniejszego niż 24. Myślę, że nie ma nadziei na równania z bardzo dużymi minimalnymi pozytywnymi rozwiązaniami, takimi jak d = 991, gdzie potrzebujemy około 100 bitów do kodowania wartości x i y. W tych przypadkach myślę, że wyspecjalizowany solver będzie działał znacznie lepiej.

BTW, strona rise4fun ma mały limit czasu, ponieważ jest to zasób udostępniony używany do uruchamiania wszystkich prototypów badawczych w grupie Wzrastanie. Aby rozwiązać nieliniowe równania Pell'a, musimy uruchomić Z3 na naszych własnych maszynach.

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)