小编Ser*_* Fe的帖子

需要帮助理解方程式

有等式Pell 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)
Run Code Online (Sandbox Code Playgroud)

结果: [y = 2744248620923429728, x = 8169167793018974721]

为什么?

PS有效答案:[y = 448036604040,x = 6224323426849]

z3 z3py

6
推荐指数
1
解决办法
901
查看次数

标签 统计

z3 ×1

z3py ×1