from z3 import *
solver = Solver()
x = BitVec('x', 64)
y = BitVec('y', 64)
# условия
constraints = [
5 + x ^ 2 == y,
y ^ 2 + x == 3
]
for i in constraints:
solver.add(i) # добавляем условия в солвер
print(solver.check()) # проверяем есть ли решение sat - решение есть, unsat - решений не существует
while solver.check() == sat:
print(solver.check())
print(solver.model()[x], solver.model()[y])# если решение есть, выводим на экран x и y
solver.add(x != solver.model()[x], y != solver.model()[y]) # добавляем условия, что новое решение на равно найденному
# Убрал +5 в первом уравнении, чтобы появились действительные корни:
equations = [
Eq(x**2, y),
Eq(y**2 + x, 3)
]
...
for result in results:
if result[x].evalf().is_real and result[y].evalf().is_real:
print('x =', result[x])
print(f'({result[x].evalf()})')
print()
print('y =', result[y])
print(f'({result[y].evalf()})')
print('\n')
我可能已经爬进了丛林，需要一个简单的算法……具体来说，这两个方程没有共同的解。这是使用 Solver Z3 的证明。您将方程式添加到条件中，变量需要在上面声明。
该算法返回 unsat，没有解决方案。例如
一种解决方案 3.5
Sympy 系统解决方案：
我们看到问题中的方程组只有复解。诚然，WolframAlfa 为这个系统提供了另外两个解决方案（可点击）：
如果不需要复杂的解决方案，请检查属性
is_real（例如result[x].evalf().is_real），并且不要考虑此属性为 False 的解决方案：结论：