我正在使用 Z3 来解决由变量的布尔约束Vi以及以下形式的约束组成的系统：
L < If(V0, T0, F0) + If(V1, T1, F1) + ... + If(Vn, Tn, Fn) <= H
其中L, H,Ti和Fi是整数常量。
尽管所有变量都是布尔变量，但我发现 QF_LIA 求解器比通用求解器要快一些，所以我使用的是前者。我的假设是 Z3 通过引入新变量和子句以显而易见的方式实现加法器来处理上述约束。但是，我自己进行转换（使用 MiniSat+）并将结果传递给 SAT 求解器需要的时间比 Z3 长一个数量级。因此，我想知道 Z3 使用什么策略来解决上述类型的系统 - 它是不是使用加法器进行转换？
Z3 使用简化为 SAT 来解决此类问题。如果您使用的是 shell，您可以提供选项-v:10（详细信息）。Z3 将显示几条描述它正在做什么的消息。对于您描述的那种问题，Z3 可能会显示以下形式的详细消息：
(lia2pb :num-exprs 9 :num-asts 185 ...)
(pb2bv :num-exprs 9 :num-asts 185 ...)
lia2pb表示 Z3 正在将线性整数算术问题转换为伪布尔约束问题。并且pb2bv意味着它将问题简化为位向量算术。
lia2pb转换在文件中实现：http
: //z3.codeplex.com/SourceControl/latest#src/tactic/arith/lia2pb_tactic.cpp
并pb2bv在文件中实现转换：http:
//z3.codeplex.com/SourceControl/latest#src/tactic/arith/pb2bv_tactic.cpp