用条件整数加法求解系统的 Z3 策略答案

【问题标题】：Z3 strategy for solving system with conditional integer additions用条件整数加法求解系统的 Z3 策略
【发布时间】：2013-09-09 19:01:11
【问题描述】：

我正在使用 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

【解决方案1】：

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

【讨论】：

感谢您的快速回复。使用详细选项 Z3 确实显示消息表明调用了 lia2pb 和 pb2bv，但是当我尝试在我的 SMT2 文件中手动调用它们时，我收到一条错误消息，提示“目标位于 pb2bv 不支持的片段中”。我使用原始文件打开了跟踪，发现实际上 Z3 没有使用 pb2bv：该策略因消息“Not pseudo-Boolean: (ite v118 (- 373266501405000) (- 653847452060000))”而中止。详细输出中没有后续消息提及策略。那么，SAT 的降幅是多少？
pb2bv 不支持任意表达式。 Z3 通常在调用lia2pb 和pb2bv 之前使用其他策略对输入进行预处理。您可以在文件z3.codeplex.com/SourceControl/latest#src/tactic/smtlogics/…中找到精确的战术顺序
策略preamble_st（在上面的文件中创建）包含 Z3 用于线性整数算术问题的基本预处理。它将消除pb2bv 不支持的几个构造。
当我尝试手动使用 pb2bv 时，我确实使用了 qflia_tactic.cpp 中的策略，包括 preamble_st 中的策略（尽管我确实收到了错误，因为 pb2bv 无法识别选项 @ 987654340@ 在mk_pb_tactic 中使用，所以我不得不删除该选项；我不确定这意味着什么）。但无论如何，我得到的“不是伪布尔...”消息是在我没有指定任何策略时：我只是将逻辑指定为 QF_LIA，断言我的约束，并调用check-sat。所以我认为这意味着 pb2bv 即使应用了预处理也失败了，而是使用了另一种策略。
我的错，你是对的，Z3 尝试在你的例子中使用pb2bv，但它失败了。 :ite-extra 选项在文件src/sat/tactic/goal2sat.cpp 中定义。它不相关，因为pb2bv 失败。如果成功，则此选项将影响 if-then-else 公式如何编码为子句。