6

方程式ペルを持っている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]

なんで？

PS有効な答え：[y = 448036604040、x = 6224323426849]

4

1 に答える 1

9

ビットベクトル演算を使用してディオファントス方程式を解くことができます。基本的な考え方はZeroExt、パッドによって指摘されたオーバーフローを回避するために使用することです。たとえば、2つのビットベクトルxとyサイズを乗算する場合、結果がオーバーフローしないように、にゼロビットをn追加する必要があります。つまり、次のように記述します。nxy

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

D(x_1, ..., x_n) = 0次のPython関数のセットを使用して、ディオファントス方程式をビットベクトル演算に「安全に」エンコードできます。「安全に」とは、エンコードに使用されるビット数に適合するソリューションがある場合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)の値を見つけxてy使用しようとします。n

次のリンクには完全な例が含まれています：http： //rise4fun.com/Z3Py/Pehp

そうは言っても、ビットベクトル演算を使用してペル方程式を解くのは非常に費用がかかります。問題は、ビットベクトルソルバーにとって乗算が非常に難しいことです。Z3で使用されるエンコーディングの複雑さは、で2次式nです。私のマシンでは、小さな解を持つペル方程式しか解けませんでした。例：d = 982、、、、。d = 980_ いずれの場合も、より小さいを使用しました。との値をエンコードするために約100ビットが必要な場合など、非常に大きな最小の正の解を持つ方程式は期待できないと思います。このような場合、専用のソルバーの方がはるかに優れたパフォーマンスを発揮すると思います。d = 1000d = 1001n24d = 991xy

ところで、rise4fun Webサイトは、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-08T02:48:37.613 に答える