各位小夥伴大家好，今天我将給大家示範一個非常進階的工具，SMT求解器。應用領域非常廣，解各類方程，解各類程式設計問題（例如解數獨），解邏輯題等都不在話下。

今天小小明就将帶大家看看這其中的精彩：

🎨z3-solver求解器🎨

🔦簡介🔫

z3-solver是由Microsoft Research(微軟)開發的SMT求解器，它用于檢查邏輯表達式的可滿足性，可以找到一組限制中的其中一個可行解，缺點是無法找出所有的可行解（對于規劃求解問題可以是scipy）。

z3-solver可應用于軟/硬體的驗證與測試、限制求解、混合系統的分析、安全、生物，以及幾何求解等問題。Z3 主要由 C++ 開發，提供了 .NET、C、C++、Java、Python 等語言調用接口，下面以python接口展開講解。

z3可直接通過pip安裝：

pip install z3-solver

參考示例：

https://ericpony.github.io/z3py-tutorial/guide-examples.htm

z3中有3種類型的變量，分别是整型(Int)，實型(Real)和向量(BitVec)。

對于整數類型資料，基本API：

Int(name, ctx=None)，建立一個整數變量，name是名字
Ints (names, ctx=None)，建立多個整數變量，names是空格分隔名字
IntVal (val, ctx=None)，建立一個整數常量，有初始值，沒名字。

對于實數類型的API與整數類型一緻，向量(BitVec)則稍有差別：

Bitvec(name,bv,ctx=None)，建立一個位向量，name是他的名字，bv表示大小
BitVecs(name,bv,ctx=None)，建立一個有多變量的位向量，name是名字，bv表示大小
BitVecVal(val,bv,ctx=None)，建立一個位向量，有初始值，沒名字。

simplify(表達式)，對可以簡化的表達式進行簡化。

完整API文檔可參考：

https://z3prover.github.io/api/html/namespacez3py.html

下面我們看看z3的基本用法：

🔀數學運算🎦

先以一個簡單例子入門：

♊️二進制一次方程♋️

比如使用z3解二進制一次方程：

$x-y = 3$

$3x-8y=4$

solve直接求解：

from z3 import *

x, y = Reals('x y')
solve(x-y == 3, 3*x-8*y == 4)

[y = 1, x = 4]

如果需要取出指定變量的結果，可以使用Solver求解器：

s=solver()，建立一個解的對象。
s.add(條件)，為解增加一個限制條件
s.check()，檢查解是否存在，如果存在，會傳回"sat"
modul()，輸出解得結果

x, y = Reals('x y')
solver = Solver()
qs = [x-y == 3, 3*x-8*y == 4]
for q in qs:
    solver.add(q)
if solver.check() == sat:
    result = solver.model()
print(result)
print("x =", result[x], ", y =", result[y])

[y = 1, x = 4]
x = 4 , y = 1

可以通過

solver.assertions()

檢視求解器已經添加的限制和限制的個數：

assertions = solver.assertions()
print(assertions)
print(len(assertions))

[x - y == 3, 3*x - 8*y == 4]
2

如果需要删除限制條件，則需要在添加限制前調用solver.push()方法。

下面我們如下方程為例進行示範：

$x > 10$

$y = x + 2$

擷取結果：

x, y = Ints('x y')
solver = Solver()
solver.add(x > 10, y == x + 2)
print("目前限制：", solver.assertions())
if solver.check() == sat:
    print("結果：", solver.model())
else:
    print(solver.check())

目前限制： [x > 10, y == x + 2]
結果： [x = 11, y = 13]

下面我們再增加一個可以被删除的限制

y < 11

：

solver.push()
solver.add(y < 11)
print("目前限制：", solver.assertions())
if solver.check() == sat:
    print("結果：", solver.model())
else:
    print(solver.check())

目前限制： [x > 10, y == x + 2, y < 11]
unsat

可以看到這種限制下，無有效解。

删除限制，再計算一次：

solver.pop()
print("目前限制：", solver.assertions())
if solver.check() == sat:
    print("結果：", solver.model())
else:
    print(solver.check())

目前限制： [x > 10, y == x + 2]
結果： [x = 11, y = 13]

⚠️注意：沒有push過的限制條件時直接pop會導緻報出 Z3Exception: b'index out of bounds' 錯誤。

🚦線性多項式限制🚧

限制條件為：

x > 2 \\

y < 10 \\

x + 2 * y = 7 \\

上述限制x和y都是整數，我們需要找到其中一個可行解：

x, y = Ints('x y')
solve([x > 2, y < 10, x + 2*y == 7])

結果：

[y = 0, x = 7]

當然，實際可行的解不止這一個，z3隻能找到其中一個可行的解。

💧非線性多項式限制🌌

$x^2 + y^2 > 3$

$x^3 + y < 5$

上述限制x和y都是實數，我們需要找到其中一個可行解：

x, y = Reals('x y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

[y = 2, x = 1/8]

很快就計算出了一個可行解。

上面我示範了一些基礎的例子，下面繼續分享綜合一些的案例：

💫高中實體勻變速直線運動相關問題📰

高中實體中的勻變速直線運動公式為：

$s=v_it + \frac12at^2$

$v_f=v_i + at$

舉個例子，以30m/s的速度前進時踩下刹車，如果減速的加速度為$-8m/s^2$，求刹車完畢時，汽車的刹車距離是多少？

直接解題：

s, v_i, a, t, v_f = Reals('s v__i a t v__f')

equations = [
    s == v_i*t + (a*t**2)/2,
    v_f == v_i + a*t,
]
print("運動方程:", equations)

variables = [
    v_i == 30,
    v_f == 0,
    a == -8
]
print("參數變量:", variables)
print("結果:")
solve(equations + variables)

運動方程: [s == v__i*t + (a*t**2)/2, v__f == v__i + a*t]
參數變量: [v__i == 30, v__f == 0, a == -8]
結果:
[a = -8, v__f = 0, v__i = 30, t = 15/4, s = 225/4]

可以看到刹車距離是225/4m，刹車曆時15/4s。

需要擷取指定變量的結果則需要Solver求解器：

solver = Solver()
equations = [
    s == v_i*t + (a*t**2)/2,
    v_f == v_i + a*t,
]
variables = [
    v_i == 30,
    v_f == 0,
    a == -8
]
solver.add(equations + variables)
if solver.check() == sat:
    result = solver.model()
print(f"刹車距離：{result[s].as_decimal(4)}m，刹車時間：{result[t].as_decimal(4)}s")

刹車距離：56.25m，刹車時間：3.75s

到這裡，大家算是已經對z3的用法入門了。下面我繼續示範一些更進階的内容，使用z3解決一些程式設計上的問題：

📜綜合性程式設計問題📈

📐解數獨✏️

之前我示範過程式自動玩數獨：

文中對于一個困難級别的數獨，python優化後的算法耗時達到3.2秒，核心邏輯使用C語言改寫後耗時達到毫秒級。

下面我使用z3求解器來解決這個問題，這樣可以在不使用其他語言開發的情況，純Python就能達到不錯的性能。

首先，我們根據數獨遊戲的規則建立限制條件：

from z3 import *

# 9x9 整數變量矩陣
X = [[Int(f"x_{i}_{j}") for j in range(9)]
     for i in range(9)]

# 每個單元格在 1,2,3,...8,9 中包含一個值
cells_c = [And(1 <= X[i][j], X[i][j] <= 9)
           for i in range(9) for j in range(9)]

# 每行每個數字最多出現一次
rows_c = [Distinct(X[i]) for i in range(9)]

# 每列每個數字最多出現一次
cols_c = [Distinct([X[i][j] for i in range(9)])
          for j in range(9)]

# 每個 3x3 方格每個數字最多出現一次
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

依然針對之前那個Python耗時3秒多的數獨：

# 需要求解的數獨，0表示空單元格
board = [
    [0, 0, 0, 6, 0, 0, 0, 3, 0],
    [5, 0, 0, 0, 0, 0, 6, 0, 0],
    [0, 9, 0, 0, 0, 5, 0, 0, 0],
    [0, 0, 4, 0, 1, 0, 0, 0, 6],
    [0, 0, 0, 4, 0, 3, 0, 0, 0],
    [8, 0, 0, 0, 9, 0, 5, 0, 0],
    [0, 0, 0, 7, 0, 0, 0, 4, 0],
    [0, 0, 5, 0, 0, 0, 0, 0, 8],
    [0, 3, 0, 0, 0, 8, 0, 0, 0]
]

求解：

def solveSudoku(board: list):
    board_c = [If(board[i][j] == 0,
                  True,
                  X[i][j] == board[i][j])
               for i in range(9) for j in range(9)]

    s = Solver()
    s.add(sudoku_c + board_c)
    if s.check() == sat:
        m = s.model()
        r = [[m[X[i][j]].as_long() for j in range(9)]
             for i in range(9)]
        return r
solveSudoku(board)

可以看到在0.3秒多的時間内已經計算出結果，而且結果與之前的結果一緻：

🍞八皇後問題🍩

有一個 8x8 的棋盤，希望往裡放 8 個棋子（皇後），每個棋子所在的行、列、對角線都不能有另一個棋子。

下圖中左圖是滿足條件的一種方法，又圖是不滿足條件的。八皇後問題就是期望找到滿足這種要求的放棋子方式：

如果我們要求找到所有滿足條件的解，則隻想使用回溯算法進行遞歸求解，但是如果隻需要一個可行解時，我們則可以使用z3求解器。

首先建立限制條件：

# 每個皇後必須在不同的行中，記錄每行對應的皇後對應的列位置
Q = [Int(f'Q_{i}') for i in range(8)]

# 每個皇後在列 0,1,2,...,7
val_c = [And(0 <= Q[i], Q[i] <= 7) for i in range(8)]

# 每列最多一個皇後
col_c = [Distinct(Q)]

# 對角線限制
diag_c = [If(i == j,
             True,
             And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
          for i in range(8) for j in range(i)]

直接求解可以得到一個可行解中，其中每個皇後的列位置：

solve(val_c + col_c + diag_c)

[Q_3 = 5,
 Q_1 = 1,
 Q_7 = 6,
 Q_5 = 2,
 Q_4 = 0,
 Q_0 = 3,
 Q_2 = 7,
 Q_6 = 4]

當然我們還可以把結果列印的清晰一點：

def print_eight_queen(result):
    for column in result:
        for i in range(8):
            if i == column:
                print(end="Q  ")
            else:
                print(end="*  ")
        print()


s = Solver()
s.add(val_c + col_c + diag_c)
if s.check() == sat:
    result = s.model()
    result = [result[Q[i]].as_long() for i in range(8)]
    print("每行皇後所在的列位置：", result)
    print_eight_queen(result)

每行皇後所在的列位置： [5, 3, 1, 7, 4, 6, 0, 2]
*  *  *  *  *  Q  *  *  
*  *  *  Q  *  *  *  *  
*  Q  *  *  *  *  *  *  
*  *  *  *  *  *  *  Q  
*  *  *  *  Q  *  *  *  
*  *  *  *  *  *  Q  *  
Q  *  *  *  *  *  *  *  
*  *  Q  *  *  *  *  *

🎡安裝依賴問題🌈

安裝程式時往往存在依賴和沖突的關系，通過z3可以輕松求解正确的包的安裝順序。

例如：

包a依賴于包b、c和z

包b依賴于包d

包c，依賴于d或e，以及f或g

包d與包e沖突

包d與包g沖突

假設要安裝包a編碼如下：

from z3 import *

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')
# 1.包a依賴于包b、c和z
q1 = And([Implies(a, dep) for dep in [b, c, z]])
# 2.包b依賴于包d
q2 = Implies(b, d)
# 3.包c，依賴于d或e，以及f或g
q3 = Implies(c, And([Or(d, e), Or(f, g)]))
# 4.包d與包e沖突
q4 = Or(Not(d), Not(e))
# 5.包d與包g沖突
q5 = Or(Not(d), Not(g))

s = Solver()
# 安裝包a
s.add(a, q1, q2, q3, q4, q5)
if s.check() == sat:
    m = s.model()
    # x() 傳回Z3表達式，x.name()傳回字元串
    r = [x.name() for x in m if is_true(m[x])]
    print("安裝a:")
    print(r)
else:
    print("無效的安裝配置")

安裝a:
['z', 'b', 'd', 'f', 'c', 'a']

為了友善調用我們可以将依賴和沖突封裝成單獨的方法：

def DependsOn(pack, deps):
    if is_expr(deps):
        return Implies(pack, deps)
    else:
        return And([Implies(pack, dep) for dep in deps])


def Conflict(*packs):
    return Or([Not(pack) for pack in packs])


def install_check(*problem):
    s = Solver()
    s.add(problem)
    if s.check() == sat:
        m = s.model()
        # x() 傳回Z3表達式，x.name()傳回字元串
        r = [x.name() for x in m if is_true(m[x])]
        print(r)
    else:
        print("無效的安裝配置")

再次調用安裝a：

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

print("安裝a:")
install_check(
    a,
    DependsOn(a, [b, c, z]),
    DependsOn(b, d),
    DependsOn(c, [Or(d, e), Or(f, g)]),
    Conflict(d, e),
    Conflict(d, g),
)

安裝a:
['z', 'b', 'd', 'f', 'c', 'a']

安裝a和g：

print("安裝a和g:")
install_check(
    a,
    g,
    DependsOn(a, [b, c, z]),
    DependsOn(b, d),
    DependsOn(c, [Or(d, e), Or(f, g)]),
    Conflict(d, e),
    Conflict(d, g),
)

安裝a和g:
無效的安裝配置

可以看到z3成功計算出存在沖突的a和g。

🎢 邏輯題🚊

在解決了程式設計問題後，我們最後玩兩道邏輯題：

🚫誰是盜賊🗿

一軍用倉庫被竊，公安部門已掌握如下線索：①甲、乙、丙三人至少有一個是竊賊；②如甲是竊賊，則乙一定是同案犯；③盜竊發生時，乙正在影劇院看電影。由此可以推出（）。

A. 甲、乙、丙都是竊賊

B. 甲和乙都是竊賊

C. 丙是竊賊

D. 甲是竊賊

完整解題代碼：

# abc分别代表甲、乙、丙是否是盜賊
a, b, c = Bools('a b c')
# 三人至少有一個是竊賊
q1 = Or(a, b, c)
# 如甲是竊賊，則乙一定是同案犯；
q2 = Implies(a, b)
# 乙一定不是
q3 = Not(b)

s = Solver()
s.add(q1, q2, q3)

options = [
    # 甲、乙、丙都是竊賊
    And(a, b, c),
    # 甲甲和乙都是竊賊
    And(a, b),
    # 丙是竊賊
    c,
    # 甲是竊賊
    a
]
result = []
for answer, option in zip("ABCD", options):
    s.push()
    s.add(option)
    print(answer, s.check(), s.assertions())
    if s.check() == sat:
        result.append(answer)
    s.pop()
print("最終答案：", "".join(result))

A unsat [Or(a, b, c), Implies(a, b), Not(b), And(a, b, c)]
B unsat [Or(a, b, c), Implies(a, b), Not(b), And(a, b)]
C sat [Or(a, b, c), Implies(a, b), Not(b), c]
D unsat [Or(a, b, c), Implies(a, b), Not(b), a]
最終答案： C

上述結果可以看到隻有第3條的結果為sat（有解），說明對應的選項 C 是正确的。

⛔️煤礦事故✴️

題目如下：

某大型煤礦發生了一起重大事故，事發現場的人有以下的斷定：

礦工甲：發生事故的原因是裝置問題；

礦工乙：有人違反了操作規程，但發生事故的原因不是裝置問題；

礦工丙：如果發生事故的原因是裝置問題，那麼有人違反操作規程；

礦工丁：發生事故的原因是裝置問題，但沒有人違反操作規程。

如果上述四人的斷定中隻有一個人為真，則以下可能為真的一項是（）。

A.礦工甲的斷定為真

B.礦工乙的斷定為真

C.礦工丁的斷定為真

D.礦工丙的斷定為真，有人違反了操作規程

E.礦工丙的斷定為真，沒有人違反操作規程

首先需要定義題目中的兩個命題，裝置是否有問題和是否有人違反操作規程。

equipment = Bool('equipment')  # 裝置是否有問題
violation = Bool('violation')  # 是否違反操作規程
qs = [
    # 甲：發生事故的原因是裝置問題；
    equipment,
    # 乙：有人違反了操作規程，但發生事故的原因不是裝置問題；
    And(violation, Not(equipment)),
    # 丙：如果發生事故的原因是裝置問題，那麼有人違反操作規程；
    Implies(equipment, violation),
    # 丁：發生事故的原因是裝置問題，但沒有人違反操作
    And(equipment, Not(violation)),
]

s = Solver()
# 上述四人的斷定中隻有一個人為真
s.add(Sum([If(q, 1, 0) for q in qs]) == 1)
# 逐個判斷各個選項是否正确
options = [qs[0], qs[1], qs[3], And(
    qs[2], violation), And(qs[2], Not(violation))]
result = []
for answer, option in zip("ABCDE", options):
    s.push()
    s.add(option)
    print(answer, s.check(), s.assertions())
    if s.check() == sat:
        result.append(answer)
    s.pop()
print("最終答案：", "".join(result))

A unsat [If(equipment, 1, 0) +
 If(And(violation, Not(equipment)), 1, 0) +
 If(Implies(equipment, violation), 1, 0) +
 If(And(equipment, Not(violation)), 1, 0) ==
 1,
 equipment]
B unsat [If(equipment, 1, 0) +
 If(And(violation, Not(equipment)), 1, 0) +
 If(Implies(equipment, violation), 1, 0) +
 If(And(equipment, Not(violation)), 1, 0) ==
 1,
 And(violation, Not(equipment))]
C unsat [If(equipment, 1, 0) +
 If(And(violation, Not(equipment)), 1, 0) +
 If(Implies(equipment, violation), 1, 0) +
 If(And(equipment, Not(violation)), 1, 0) ==
 1,
 And(equipment, Not(violation))]
D unsat [If(equipment, 1, 0) +
 If(And(violation, Not(equipment)), 1, 0) +
 If(Implies(equipment, violation), 1, 0) +
 If(And(equipment, Not(violation)), 1, 0) ==
 1,
 And(Implies(equipment, violation), violation)]
E sat [If(equipment, 1, 0) +
 If(And(violation, Not(equipment)), 1, 0) +
 If(Implies(equipment, violation), 1, 0) +
 If(And(equipment, Not(violation)), 1, 0) ==
 1,
 And(Implies(equipment, violation), Not(violation))]
最終答案： E

這些就是z3求解器那些常見的應用，你學費了嗎？還想學習python解決規劃求解問題，記得關注我等待下一期噢~

我是小小明，咱們下期再見~

z3-solver求解器🎨z3-solver求解器🎨

🎨z3-solver求解器🎨

🔦簡介🔫

🔀數學運算🎦

♊️二進制一次方程♋️

🚦線性多項式限制🚧

💧非線性多項式限制🌌

💫高中實體勻變速直線運動相關問題📰

📜綜合性程式設計問題📈

📐解數獨✏️

🍞八皇後問題🍩

🎡安裝依賴問題🌈

🎢 邏輯題🚊

🚫誰是盜賊🗿

⛔️煤礦事故✴️

繼續閱讀

【python】【資料處理】畫多元資料分布圖

mybatis_入門程式Mybatis入門

線性表之順序表的實作

AOP程式設計_Android優雅權限架構(1)概念基礎，2021金三銀四前言正文大綱正文

Effective Java 8:通用程式設計

C++判斷素數、求最大公約數代碼判斷一個數是否為素數求兩個數的最大公約數

SequoiaDB巨杉資料庫C++驅動概述

OOM三種類型

工廠模式-三種類型

【python】netconf協定對接管理裝置

「Python 網絡自動化」NETCONF —— Python 使用 NETCONF 管理配置 H3C 網絡裝置

【遞歸】高效率求2的n次幂

win10本地scala和spark安裝安裝scala安裝spark

scala (3) Function 和 Method

在python中建立excel并寫入

hdu7108哈希