Python花式解方程

numpy

numpy 用來解方程的話有點複雜，須要用到矩陣的思惟！我矩陣沒學好再加上 numpy 不能解非線性方程組，因此...我也不會這玩意兒！

sympy

遜色於 sage 和 z3，但解方程也是很是不錯的！

from sympy import *
x = symbols('x')
y = symbols('y')
res = solve([x+y-3,x-y-1],[x,y])[0]
print(res)

sage

sage 既能解線性方程組，又能解非線性方程組，堪稱解方程界的神器，可是表達式不支持位運算，好比：與或非，取餘以及異或。出現位運算的方程就只能用 z3 建立約束求解！sage 的優勢也很明顯：表達式簡單易寫，運算速度快！
在線sage求解

var('x y')
solve([x**3+y**2+666==142335262,x**2-y==269086,x+y==1834],[x,y])

z3

z3 也叫約束求解器，用來解任何方程都沒有問題！可是 windows 不太好裝，因此我基本上是在linux上跑，python2 和 python3 都支持！使用的思路很是簡單：

• 先建立你所需類型的符號變量
• 再初始化一個約束器，
• 添加約束
• 最後判斷約束是否有解以及求解變量

下面列舉經常使用的函數，順便給個 z3-solver文檔

# 符號變量類型
Int('x')
Real('x')
Bool('x')
BitVec('x',N) # N bit的符號變量，用於位操做
BitVecVal(num,N) # N bit的數據 num
# 初始化約束器
solver = Solver()
# 添加約束
solver.add(x+y==10,x-y==0)
# 求解約束
solver.check()
ans = solver.mode()

# 初始化多個符號變量
x = [Int('x%d' % i) for i in range(n)]
# 取結果中某個變量的值
value = ans[x].as_long()

END