Z3的旧版本与新版本 [英] old vs new version of Z3

问题描述

我有一个实例，旧版本的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文件中大约有50,000行，所以我不能在这里发布它。如果有人感兴趣，我很乐意通过电子邮件发送文件。 谢谢。

推荐答案

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

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

在"工作进行中"分支中，我通过使用

成功地重现了Z3 2.19的性能

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

Here是有关如何下载"正在进行的工作"分支的说明。

要获得相同的行为，我们还必须替换 (Check-Sat) 使用 (Check-Sat-Using SMT)

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

            (set-option :auto-config false)

而不是

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

这篇关于Z3的旧版本与新版本的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！