Z3求解器的使用

因为项目需要，这里需要实现一些SMT编码对问题的求解工作。

主流的求解器可以使用Z3

Z3Prover/z3: The Z3 Theorem Prover (github.com)

我们此次尝试使用Python、Java版本的求解器进行学习。

因为本地环境为Windows且安装了visual studio

但是我们自己工作时，缺失nmake文件，

NMAKE is not recongnizing in developer command prompt vs2019 - Developer Community (visualstudio.com)查询后得知，我们的vs中没有安装必要的c++生成工具，安装必要组件，将该组件添加至环境变量并重启.

可以运行了，但是报错。

由于Z3开发版本是C++17，我们要在vs中确认库文件的匹配。

卸载vs2022，安装vs2019

---

在安装完毕vs2019，配置环境变量之后。

终于可以顺利编译 

但是最后报错：

模块计算机类型“X86”与目标计算机类型“X64”冲突的原因分析与解决方案_咸鱼半条的博客-CSDN博客

可以理解为我们本身平台是64位的没问题，模块计算机是x86的

visual c++ - fatal error LNK1112: module machine type 'x64' conflicts with target machine type 'X86' - Stack Overflow

这个问题可能是因为您正在尝试使用一个在Windows x64平台上编译的模块，但是您的目标计算机是x86平台。为了解决这个问题，您需要重新编译模块以匹配目标计算机的类型。具体来说，您需要使用该平台的编译器来重新编译该模块。如果您使用的是Visual Studio，您需要在命令行中使用适当的编译器选项来指定目标计算机的体系结构。例如，如果您的目标计算机是x86平台，您可以使用"nmake /f Makefile.win TARGET_CPU=X86"命令来编译该模块。如果您仍然遇到问题，请尝试查找关于模块如何编译和配置的更多信息。 

 我们清空z3的文件夹，用脚本生成32位文件，然后再配合msvc x86的nmake进行测试

终于成功：

 可以看到提示：

Z3 was successfully build.

并且提示，我们已经可以结合路径来执行z3py的脚本了。

---

问题又来了，我们目的是用Java语言或Python语言编写程序，那么

我们需要生成响应的bindings，所以我们重新生成Java支持的文件。

 这里会报错，一些路径支持并没有配置好：

我们已经build完毕需要的cpp文件，但是仍然出错，这个问题后面在继续调研。

---

但是实际上，我目前最常用的还是用python-z3，

因为只需要执行pip install z3-solver即可，如果由于网络问题，我们只需要执行

pip install z3-solver -i https://pypi.tuna.tsinghua.edu.cn/simple

即可。

---

有了Python的支持，我们可以进一步开始学习如何用Z3工具求解我们感兴趣的问题：

问题1:

#coding:utf8
from z3 import *
 
# 首先创建一个求解器
s = Solver() 
 
'''
比如我们想求解这么一个问题
x + y = 5
x >= 2
y >= 2
我们想看看符合要求的x，y的整数解有哪些？
'''
 
# 定义两个变量
x = Int('x')
y = Int('y')
 
# 在求解器中定义约束条件
s.add(x >= 2)
s.add(y >= 2)
s.add(x + y == 5)
 
# 我们调用求解器的check()方法来判别约束集合是否能得到可行解，如果可行，给出结果
print(s.check())
if s.check():
    m = s.model()
    print(m)
 
'''
输出：
sat
[y = 2, x = 3]
'''

问题2：

#coding:utf8
'''
smt问题可以理解为很多逻辑谓词的组合，我们可以做一些问题的推理工作
比如有这么一个问题
Alice and Bob can complete a job in 2 hours.
Alice and Charlie can complete the same job in 3 hours
Bob and Charlie can complete the same job in 4 hours
How long will the job take if Alice, Bob, and Charlie work together?Assume each person works at a constant rate, whetherworking alone or working with others.
'''
 
from z3 import *
s = Solver()
 
a, b, c, n = Reals('a b c n')
 
s.add(a * 2 + b * 2 == 1)
s.add(a * 3 + c * 3 == 1)
s.add(b * 4 + c * 4 == 1)
s.add(a * n + b * n + c *n == 1)
 
print(s.check())
if s.check() == sat:
    m = s.model()
    print(m)
 
'''
输出：
sat
[n = 24/13, c = 1/24, a = 7/24, b = 5/24]
'''

问题3：

#coding:utf8
'''
Two candles of equal heights, but different thicknesses, are lit.
The first burns off in 8 hours and the second in 10 hours.
How long after lighting, in hours, will the first candle be half the height of the second candle?
The candles are lit simultaneously and each burns at a constant linear rate.
'''
 
from z3 import *
 
s = Solver()
 
# c1代表第一个蜡烛的高度，c2代表第二个蜡烛的高度，t代表时间
c1, c2, t = Reals('c1 c2 t')
 
s.add(c1 == 1 - t / 8)
s.add(c2 == 1 - t / 10)
 
s.add(c1 > 0)
s.add(c2 > 0)
 
s.add(c1 * 2 == c2)
 
print(s.check())
if s.check() == sat:
    m = s.model()
    print(m)
 
'''
输出：
sat
[t = 20/3, c1 = 1/6, c2 = 1/3]
'''

我们创建求解器，将我们的内容转换为z3可以理解的约束，然后再调用check方法即可进行求解。

---

参考资料：

(13) Solving Mind Your Decisions Problems using Z3 - YouTube