因為項目需要使用z3庫來解決問題，所以自己學習了一下，結果發現網上教程比較少，而且大部分都是使用Python，而我本人是C++的忠實信徒，在知道C++也可以使用z3庫以后我毫不猶豫地著手用C++使用z3，但是我很快發現，網上基本沒有關于C++使用z3的教程（中文社區一點都沒有），因此我記錄一下我自己的學習過程希望能夠幫助到其他學習的人。

教程鏈接

網上現有的有三個教程：
官方example.cpp文檔：https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp
入門筆記：
http://www.cs.utah.edu/~vinu/research/formal/tools/notes/z3-notes.html
API接口：
https://z3prover.github.io/api/html/group__cppapi.html

其中主要教程是官方的example.cpp
第二個入門教程也非常不錯，里面包含了環境的搭建，例子的說明（其實就是example.cpp的說明）
第三個API沒有什么用覺得

不過上面的教程都沒有說如何在一個普通文件中使用z3庫，我在StackOverflow上找到一個回答解決了這個問題：https://stackoverflow.com/questions/17514923/need-help-in-using-z3-api-in-a-c-program。簡單來講在install之后要在文件中包含z3++.h頭文件，而且在編譯參數上要加上-lz3

我一開始是學習使用Python使用z3的，因此也發現一些很好的教程，其中對我幫助最大的是一個用z3解決背包問題的博客，讓我明白如何用z3解決極值問題：https://blog.csdn.net/weixin_41950078/article/details/111416573

性能測試

同時我測試了Python和C++的性能差距，以上面學習到的01背包問題為例，在數據量為40的時候，Python的運行時間是5830.4131779670715s（我沒有寫錯），C++的運行時間是57s。
希望的我的測試能夠堅定大家用C++使用z3庫的決心（狗頭
下符測試代碼和運行截圖：

Python

測試代碼

import timefrom z3 import *
def zero_one_knapsack(weights, values, cap):solver = Optimize()# the decision variablesflags = [Int(f"x_{i}") for i in range(len(weights))]for flag in flags:solver.add(Or(flag == 0, flag == 1))weight_arr = []i = 0for w in weights:weight_arr.append(w * flags[i])i += 1# add weight constraintsolver.add(sum(weight_arr) <= cap)value_arr = []i = 0for v in values:value_arr.append(v * flags[i])i += 1solver.maximize(sum(value_arr))start = time.time()# calculateresult = solver.check()print(f"use {time.time() - start}s to calculate")if result == sat:model = solver.model()print("\n".join([f"Index: {index}, weight: {weights[index]}, value: {values[index]}"for index, flag in enumerate(flags) if model[flag] == 1]))else:print("empty")if __name__ == '__main__':C = 300W = [71,34,82,23,1,88,12,57,10,68,5,33,37,69,98,24,26,83,16,26,18,43,52,71,22,65,68,8,40,40,24,72,16,34,10,19,28,13,34,98]V = [26,59,30,19,66,85,94,8,3,44,5,1,41,82,76,1,12,81,73,32,74,54,62,41,19,10,65,53,56,53,70,66,58,22,72,33,96,88,68,45]zero_one_knapsack(W, V, C)

運行結果

C++

運行代碼

#include <iostream>
#include <typeinfo>
#include <string>
#include <z3++.h>
#include <vector>
#include <ctime>using namespace z3;
using std::cout;
using std::cin;
using std::endl;
using std::string;
using std::vector;void knapsack(const vector<int> &weights, const vector<int> &values, int cap) 
{context c;optimize opt(c);vector<expr> flags;for (decltype(weights.size()) i = 0; i < weights.size(); ++i) {flags.push_back(c.int_const( ("x" + std::to_string(i)).c_str() ));}for (auto &flag : flags) {opt.add(flag == 0 || flag == 1);}expr tmp = c.int_const("tmp");tmp = c.int_val(0);for (decltype(weights.size()) i = 0; i < weights.size(); ++i) {tmp = tmp + weights[i] * flags[i];}opt.add(tmp <= cap);tmp = c.int_val(0);for (decltype(values.size()) i = 0; i < values.size(); ++i) {tmp = tmp + values[i] * flags[i];}opt.maximize(tmp);//cout << opt << endl;clock_t begin = clock();auto result = opt.check();clock_t end = clock();if (result == sat) {model m = opt.get_model();//cout << m << endl;for (unsigned i = 0; i < flags.size(); ++i) {auto item = flags[i];if (m.eval(item).get_numeral_int() == 0) continue;cout << i << ":\t"  << weights[i] << "\t" << values[i] << endl;}} else {cout << "no solution" << endl;}cout << "cost time:" << static_cast<double>(end - begin) / CLOCKS_PER_SEC << "s" << endl;
}void work()
{vector<int> W,V;int C,n,w,v;cin >> C >> n;while (n--) {cin >> w >> v;W.push_back(w);V.push_back(v);}knapsack(W, V, C);
}int main()
{std::ios::sync_with_stdio(false);work();return 0;
}

為了在輸出結果的時候判斷是否選擇該物品需要從model中獲取結果，但是我不知道如何比較結果是否為0（在程序中0表示不選），在網上找來找去都沒有，最后沒有辦法只能自己嘗試，終于在成員列表里面找到了一個好像能夠把expr轉換成int的函數，即上面的if (m.eval(item).get_numeral_int() == 0) continue;語句，卡了好久，沒有教程太慘了。

運行結果