Z3是由微软研究开发的一款强大的求解器，用于解决逻辑公式和约束条件的问题。Z3在约束求解、混合系统分析、安全领域、生物学和几何问题等多个领域都有广泛的应用。

求解器安装

pip install z3-solver

基础求解案例

z3求解器使用非常简单，代码也简洁容易理解。直接从一些案例，来看看z3求解器的基础使用。

声明整数变量并求解

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

输出：

实数非线性约束求解

from z3 import *
x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

输出：

无解问题

以下问题是无解，看看输出显示。

from z3 import *
x = Real('x')
y = Real('y')
solve(x > 4, y < 0,y >-1,x+y <3)

输出：

解决数独问题

数独问题是一个非常流行的谜题。目标是在框中插入数字以仅满足一个条件：每行、每列和 3*3 框必须包含数字 1 到 9 正好一次。

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print ("failed to solve")