2

我与 Z3 和 Yices 合作了不到一年的时间来解决一些研究问题。使用这些求解器时，我总是需要评估性能，尤其是两件事：建模/检查所需的时间和空间（内存）（可满足性）。在 Z3 的情况下，我没有找到直接找到它们的线索。我尝试使用“statistics”（使用 Z3 NET API 提供的函数“DisplayStatistics”），发现输出如下所示（例如）：

编号。冲突：122

编号。决定：2245

编号。传播：27884（二进制：21129）

编号。重启：1

编号。最终检查：1

编号。分钟。点亮：52

编号。添加等式：3766

编号。mk 布尔变量：2782

编号。德尔布尔变量：658

编号。mk 节点：1723

编号。删除节点：78

编号。MK 条款：3622

编号。删除条款：1517

编号。mk bin 条款：3067

编号。MK 点亮：18935

编号。ta 冲突：28

编号。添加行：5091

编号。枢轴：328

编号。断言更低：2597

编号。断言上：3416

编号。断言diseq：1353

编号。绑定道具：787

编号。固定当量：697

编号。偏移量：866

编号。伪 nl.: 34

编号。等式。适配器：820

我不知道如何解释这些值以了解使用的内存/时间。有一些方法可以找到运行时间（使用秒表等计时器类）。但是，在空间要求的情况下，我没有找到任何方法。如果我可以获得建模所需的布尔变量（低级，SAT 求解器）的数量，那么对我来说效果很好。

如果有人能告诉我解决方案，那就太好了。

4

1 回答 1

2

你用的是哪个版本的Z3？最新版本（Z3 3.2）包括内存消耗统计。它将显示为max. heap size。话虽如此，评估 Z3 性能的最佳方法是使用z3.exe. Z3 可执行文件将报告时间和内存消耗。此外，一些性能改进尚无法通过 API 获得。

对于一些应用程序，文本界面是理想的选择。也就是说，您的应用程序使用 SMT 2.0 命令通过管道与 Z3 进程通信。主要优点是：使用不同的 SMT 求解器并进行比较非常容易；很容易杀死Z3并重新启动它；您可以创建几个不同的进程；如果 Z3 死了，您的应用程序不会死。当然，这种解决方案不适合执行数千个简单查询或需要与 Z3 紧密集成（例如Scala^Z3）的应用程序。

于 2011-12-30T16:16:56.467 回答