在特定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

回答

相關問題