0

我有一个实例可以通过旧版本的 Z3（版本 2.18）非常有效地解决。它会在几秒钟内返回 SAT。但是，当我在当前版本的 Z3（版本 4.3.1）上尝试时。10 分钟后它不会返回任何结果。

以下是有关该实验的一些细节。有人可以给点建议吗？

  • 有 4000 个 Bool 变量和 200 个 Int 变量

  • 所有约束都在命题逻辑中，并在整数之间进行比较，例如 a < b

  • 平台：open suse linux 12.3@thinkpad T400s

  • Z3 v2.18 是去年作为 linux 二进制文件下载的（我现在找不到链接）

  • Z3 v4.3.1 作为源代码下载，我在笔记本电脑上使用默认设置编译它

smt文件大概有50000行，这里就不贴了。如果有人感兴趣，我很乐意通过电子邮件发送文件。谢谢。

4

1 回答 1

1

Z3 是一组求解器。默认配置因版本而异。进步从来不是单调的。也就是说，一个新版本可能会解决更多的问题，但可能会更慢，并且在某些问题上会失败。

备注：作者已通过电子邮件将他的基准发送给 Z3 作者。

在“work-in-progress”分支中，我设法重现了 Z3 2.19 的性能，方法是使用

            (set-option :smt.auto-config false)

以下是有关如何下载“正在进行的工作”分支的说明。

为了获得相同的行为，我们还必须将 (check-sat) 替换为 (check-sat-using smt)

顺便说一句，在正式版本中，我们必须使用

            (set-option :auto-config false)

代替

            (set-option :smt.auto-config false)
于 2013-10-13T17:25:30.380 回答