在特定QF_LRA实例上加速Z3

我在QF_LRA中遇到了问题，MathSAT5可以快速解决问题（不满意，< 5分钟），但Z3似乎没有多大进展（即使在7天后也没有结果）。这可以通过Z3中的一些设置来解决吗？在特定QF_LRA实例上加速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

这使得全球的重写规则（除2015年SMT竞争的应用程序跟踪设置）。

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

首先，得到Z3来解决这个问题是非常好的。作为下一步，我还想提取一个不可靠的核心，如果这对你的tipps很重要。

非常感谢提前！

来源

2016-01-13 cgeist

更换(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。

来源

2016-01-13 15:24:32 mmpourhashem

优秀的答案！非常感谢！！我看了一下教程和（帮助策略），但仍然很难找到我自己的配置。有更详细的教程吗？ – cgeist

顺便说一句：即使启用了核心提取，解决时间也只是低于3分钟，这非常棒。再次感谢！ – cgeist

查看Leonardo de Moura等人的论文[“SMT解决方案中的战略挑战”]（http://link.springer.com/chapter/10.1007/978-3-642-36675-8_2）。人。为了找到最佳配置，最好在调试模式下编译Z3并检查Z3在每个步骤之后究竟在做什么（简化，求解方程，...）。检查莱昂纳多的答案[这里]（http://stackoverflow.com/questions/13102789/printing-internal-solver-formulas-in-z3/13103031#13103031）。 – mmpourhashem

在特定QF_LRA实例上加速Z3

回答

相关问题