用z3的api修正例程并中文化
之前搭原型时,发现了 这个问题向z3定理证明库的开发组请教,原来应使用其 API 而非 Python 的原生逻辑运算符。
将 原始例程 修正并中文化后如下。
z3 版本
仍在 python 3.12 下测试。
import z3
## You can install z3 using the following command:
## pip3 install z3-solver
s = z3.Solver()
甲, 戊, 丁, 乙, 丙 = z3.Bools(
["甲", "戊", "丁", "乙", "丙"]
)
# 1. 至少一个有问题
s.add(z3.Or(甲, 丁, 乙, 丙, 戊))
# 2. 若甲有问题,且乙没问题
# 则戊有问题
s.add(z3.If(
z3.And(甲, z3.Not(乙)), # condition
戊, # then
True)) # else
# 3. 若甲没问题, 则丙没问题
s.add(z3.If(z3.Not(甲), z3.Not(丙), True))
# 4. 若乙有问题, 则丙有问题
s.add(z3.If(乙, 丙, True))
# 5. 甲和乙都有问题不可能
s.add(z3.Not(z3.And(甲, 乙)))
# 6. 除非乙有问题否则戊没问题
s.add(z3.If(乙, True, z3.Not(戊)))
# 输出解答
if s.check() != z3.sat:
raise ValueError("无解")
print(s.model())
输出:
[甲 = False, 乙 = False, 丙 = False, 丁 = True, 戊 = False]
Prolog 版本
在线环境 运行 ?- 侦查(X甲, X戊, X丁, X乙, X丙)
。
有问题 :- true.
没问题 :- false.
侦查(X甲, X戊, X丁, X乙, X丙):-
% 每人没问题或有问题
member(X甲, [有问题, 没问题]),
member(X戊, [有问题, 没问题]),
member(X丁, [有问题, 没问题]),
member(X乙, [有问题, 没问题]),
member(X丙, [有问题, 没问题]),
% 1. 至少一个有问题
(X甲 = 有问题
; X戊 = 有问题
; X丁 = 有问题
; X乙 = 有问题
; X丙 = 有问题),
% 2. 若甲有问题,且乙没问题
% 则戊有问题
((X甲 = 有问题, X乙 = 没问题) % 如果
-> X戊 = 有问题 % 则
; true), % 否则
% 3. 若甲没问题, 则丙没问题
(X甲 = 没问题 -> X丙 = 没问题; true),
% 4. 若乙有问题, 则丙有问题
(X乙 = 有问题 -> X丙 = 有问题; true),
% 5. 甲和乙都有问题不可能
not(X甲 = 有问题), not(X乙 = 有问题),
% 6. 除非乙有问题否则戊没问题
(X乙 = 有问题 -> true; X戊 = 没问题),
true.
输出:
X丁 = 有问题,
X丙 = X乙, X乙 = X戊, X戊 = X甲, X甲 = 没问题
对比
语法相似:
prolog 版本里的这句 not(X甲 = 有问题), not(X乙 = 有问题),
还是带疑惑,没找到如果要表达「甲没问题,乙也没问题」该怎么写。
https://github.com/Z3Prover/z3/issues/7724
I found a weird issue when trying out the sample.
After checking the tutorial, I replaced the or clause with Or:
s.add(z3.Or(Chase, Heath, Mullaney, Ellis, Decker))
And the issue is gone. I wonder what’s the difference between z3.Or and the python or?
NikolajBjorner commented on Jul 8, 2025 NikolajBjorner on Jul 8, 2025 Contributor
python or: not translated to z3. z3.Or: translated to z3.
We don’t overload “or” in the BoolRef class in python. Not sure if it is desired/possible.