necesita ayuda para entender la ecuación

Question

Tener la ecuación de Pell x*x - 193 * y*y = 1

en z3py:

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

Resultado: [y = 2744248620923429728, x = 8169167793018974721]

¿Por qué?

P.S. Válida respuesta: [y = 448036604040, x = 6224323426849]

Answer 1

Es posible utilizar la aritmética de bits y vectores para resolver ecuaciones diofánticas. La idea básica es usar ZeroExt para evitar los desbordamientos señalados por Pad. Por ejemplo, si multiplicamos dos vectores de bit x y y del tamaño n, entonces debemos agregar n bits cero a x y y para asegurarnos de que el resultado no se desborde. Es decir, se escribe:

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

El siguiente conjunto de funciones de Python se puede utilizar para "segura" codificar cualquier ecuación Diophantine D(x_1, ..., x_n) = 0 en la aritmética de bits en vectores. Con "seguridad", me refiero a si hay una solución que se ajusta al número de bits utilizados para codificar x_1, ..., x_n, entonces eventualmente se encontrarán recursos de módulo como memoria y tiempo. Usando esta función, podemos codificar la ecuación de Pell x^2 - d*y^2 == 1 como eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))). La función pell(d,n) intenta encontrar valores para x y y usando n bits.

El siguiente enlace contiene el ejemplo completo: http://rise4fun.com/Z3Py/Pehp

Dicho esto, es muy cara para resolver la ecuación de Pell usando aritmética de bits en vectores. El problema es que la multiplicación es realmente difícil para el solucionador de bit-vector. La complejidad de la codificación utilizada por Z3 es cuadrática en n. En mi máquina, solo pude resolver las ecuaciones de Pell que tienen pequeñas soluciones. Ejemplos: d = 982, d = 980, d = 1000, d = 1001. En todos los casos, utilicé un n más pequeño que 24. Creo que no hay esperanza para ecuaciones con soluciones positivas mínimas muy grandes como d = 991 donde necesitamos aproximadamente 100 bits para codificar los valores de x y y. Para estos casos, creo que un solucionador especializado funcionará mucho mejor.

Por cierto, el sitio web rise4fun tiene un tiempo de espera pequeño, ya que es un recurso compartido utilizado para ejecutar todos los prototipos de investigación en el grupo Rise. Entonces, para resolver ecuaciones de Pell no triviales, necesitamos ejecutar Z3 en nuestras propias máquinas.

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)