Z3 - 第一次簡單小練習

Z3,打 CTF 好用工具

這是我前陣子學到的好用工具 - Z3
解 CTF 某些題目真的爆快XD
那麼深入的解題我還沒學會
但基礎的解國中數學二元一次方程式之類也超快,可以拿來做簡單小練習,增加爽快感

故事起因於我的母親傳給我一張那種長輩們都會流傳的奇怪數學圖
通常這種圖片都是耍人的腦筋急轉彎型
但我非常認真的當作一般數學題目將代數代入
看到題目長這樣

a + b = 12
c - d = 9
a + c = 22
b + d = 12

嗯?
這好像可以拿來用 Z3 玩玩看欸!!
於是開始拿之前的範例數學題做修改

卡在該怎麼宣告未知數
之前練習題的未知數是用Int宣告
已知這題的四個變數都是有小數點的(已手動算完XD)
其實這邊有用Int硬試試看
會跳出 error 表示解不開
Float試試看,結果跳出沒有這種宣告的 error 訊息
查了一些簡單範例
發現有一種宣告方式是Real
應該是 “實數” 的意思,可以試試看

補充一下數學中所謂的 “實數”

實數,是有理數和無理數的總稱,前者如0、-4、81/7;後者如√2、π等。

以上取自維基百科第一行

z3-demo.py

#!/usr/bin/env python

from z3 import *

a = Real('a')
b = Real('b')
c = Real('c')
d = Real('d')

s = Solver()
s.add(a + b == 12)
s.add(c - d == 9)
s.add(a + c == 22)
s.add(b + d == 12)

print(s.check())
print(s.model())
$ python z3-demo.py
sat
[b = 11/2, a = 13/2, c = 31/2, d = 13/2]

收工