如何找到 Z3 (NET API) 中建模/检查可满足性所需的内存和时间
我与 Z3 和 Yices 合作了不到一年的时间来解决一些研究问题。使用这些求解器时，我总是需要评估性能，尤其是两件事：建模/检查（可满足性）所需的时间和空间（内存）。对于Z3，我没有找到直接找到它们的线索。我尝试使用“统计”（使用 Z3 NET API 提供的“DisplayStatistics”功能），并发现输出如下所示（例如）：
编号。冲突：122
编号。决定：2245
编号。传播：27884（二进制：21129）
编号。重新启动：1
编号。最终检查：1
编号。分钟。升数：52
编号。添加方程式：3766
编号。 mk 布尔变量：2782
编号。德尔布尔变量：658
编号。 mk 节点：1723
编号。删除节点：78
编号。 mk 条款：3622
编号。 del 子句：1517
编号。 mk bin 子句：3067
编号。 mk 灯数：18935
编号。 ta 冲突：28
编号。添加行：5091
编号。枢轴：328
编号。断言下限：2597
编号。断言上限：3416
编号。断言 diseq: 1353
编号。绑定道具：787
编号。固定方程：697
编号。偏移量：866
编号。伪 nl.: 34
编号。等式适配器：820
我不知道如何解释这些值以了解已使用的内存/时间。有某种方法可以找到运行时间（使用计时器类，如秒表）。但是，在空间需要的情况下，我没有找到任何方法。如果我可以获得建模所需的布尔变量（低级，SAT 求解器）的数量，那么对我来说效果会很好。
如果有人能告诉我解决方案，那就太好了。
I am working with Z3 and Yices for less than a year for solving some research problems. Working with these solvers, I always need to evaluate the performance, especially two things: time and space (memory) required for modeling/checking (the satisfiability). In case of Z3, I found no clue to find them directly. I tried with the "statistics" (using the function "DisplayStatistics" provided by Z3 NET API), and found the output as shown (e.g.) below:
num. conflicts: 122
num. decisions: 2245
num. propagations: 27884 (binary: 21129)
num. restarts: 1
num. final checks: 1
num. min. lits: 52
num. added eqs.: 3766
num. mk bool var: 2782
num. del bool var: 658
num. mk enode: 1723
num. del enode: 78
num. mk clause: 3622
num. del clause: 1517
num. mk bin clause: 3067
num. mk lits: 18935
num. ta conflicts: 28
num. add rows: 5091
num. pivots: 328
num. assert lower: 2597
num. assert upper: 3416
num. assert diseq: 1353
num. bound prop: 787
num. fixed eqs: 697
num. offset eqs: 866
num. pseudo nl.: 34
num. eq. adapter: 820
I do not know how to interpret these values to understand the used memory/time. There is some way to find the running time (using timer classes like Stopwatch). But, in case of space requirement, I did not find any way. If I can get the number of Boolean variables (low level, SAT solver) required for modeling could work very well for me.
It would be great, if anyone can show me the solution.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您使用的是哪个版本的 Z3？最新版本（Z3 3.2）包括内存消耗统计信息。它将显示为
max。堆大小。话虽这么说，评估 Z3 性能的最佳方法是使用z3.exe。 Z3 可执行文件将报告时间和内存消耗。此外，一些性能改进还无法通过 API 实现。对于多种应用程序来说，文本界面是理想的选择。也就是说，您的应用程序通过管道使用 SMT 2.0 命令与 Z3 进程进行通信。主要优点是：很容易使用不同的SMT求解器并进行比较；很容易杀死Z3并重新启动它；您可以创建多个不同的流程；如果 Z3 死掉，你的应用程序不会死掉。当然，此解决方案不适用于执行数千个简单查询或需要与 Z3 紧密集成的应用程序（例如 Scala^Z3）。
Which version of Z3 are you using? The latest version (Z3 3.2) includes memory consumption statistics. It will be displayed as
max. heap size. That being said, the best way to evaluate Z3's performance is to usez3.exe. The Z3 executable will report time and memory consumption. Moreover, some performance improvements are not yet available through the API.For several applications the textual interface is the ideal option. That is, your application communicates with the Z3 process using SMT 2.0 commands through a pipe. The main advantages are: it is very easy to use different SMT solvers and compare them; it is easy to kill Z3 and restart it; you can create several different processes; if Z3 dies your application does not die. Of course, this solution is not good for applications that perform thousands of easy queries, or require a tight integration with Z3 (e.g.
Scala^Z3).