Z3的新旧版本

Question

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

以下是有关该实验的一些详细信息。谁能给点建议？

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

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

• 平台：打开 suse linux 12.3@thinkpad T400s

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

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

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

Answer 1

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

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

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

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

Here 是关于如何下载“work-in-progress”分支的说明。

要获得相同的行为，我们还必须替换 （检查周六） 和 (check-sat-using smt)

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

            (set-option :auto-config false)

而不是

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