在特定 QF_LRA 个实例上加速 Z3

Question

我在 QF_LRA 中遇到了一个问题，MathSAT5 出人意料地迅速解决了这个问题（unsat，< 5 分钟），但 Z3 似乎没有取得太大进展（即使在 7 天后也没有结果）。这可以通过 Z3 中的某些设置来解决吗？

它包含（大致）这 5 种类型的许多子句：

(assert (or (< p47a2 p8a2) (< (+ p47a0 p47a2) (+ p8a0 p8a2)) (< (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)) (and (= p47a2 p8a2) (= (+ p47a0 p47a2) (+ p8a0 p8a2)) (= (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)))))
(assert (= 1.0 (+ p3887a0 p3887a1 p3887a2 p3887a3)))
(assert (>= p1715a0 0.0))    
(assert (= p133a2 p133a1))
(assert (or (= p379a1 0.0) (= p379a2 0.0)))

可以从 here 下载 SMT2 格式的完整问题实例。

用 MathSAT 求解的关键是设置

preprocessor.simplification=8

启用全局重写规则（除了SMT 2015竞赛的应用程序轨道设置）。

Z3 中有什么类似的东西我可以试试吗？或者您建议我执行的任何编码预处理/优化？我对 SMT 比较陌生；因此任何 help/guidance 将不胜感激。

首先让Z3解决这个问题会很棒。作为下一步，我还想提取一个不饱和的核心，如果这对你的小费很重要的话。

非常感谢！！

Answer 1

将(check-sat)替换为

(check-sat-using (then simplify solve-eqs (! smt :case_split 0 :relevancy 0 :auto_config false :restart_strategy 2)) :print_model true)

Z3一分钟搞定。但是，你可以找到更好的配置 here.

在特定 QF_LRA 个实例上加速 Z3

Speeding up Z3 on specific QF_LRA instances

z3