Z3:非线性算法的奇怪行为 [英] Z3 : strange behavior with non linear arithmetic
问题描述
我刚刚开始使用Z3(v4.4.0)，我想尝试其中一个教程示例:
(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
如前所述，第二个示例以未知"失败，并且通过将详细级别提高到3，我认为我理解为什么:简化过程中出现一些问题，则该策略失败了. 为了更好地了解问题(并缩短输出)，我决定删除代码的第一部分以仅测试失败的部分:
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
但神奇的是，现在我得到了星期六".我不确定Z3在进行非线性算术时如何选择其策略，但是问题可能出在Z3为第一个公式选择策略而对第二个公式没有用吗?
预先感谢
第二种编码与第一种编码不等效，因此行为不同.第二种编码不包括约束(assert (> (* a a) 3))，因此Z3可以发现，对于实数b和c的某些选择，b ^ 3 + b * c = 3是可满足的.但是，当它对某个整数a具有a ^ 2> 3的约束时，即使两个断言彼此独立，也找不到令人满意的结果.
对于此问题，本质上是Z3在遇到实数与整数混合时，默认情况下将不使用非线性实数算术求解器(已完成).这是一个使用qfnra-nlsat(rise4fun链接: http://rise4fun.com/Z3/KDRP ):
(declare-const a Int)
;(assert (> (* a a) 3))
;(check-sat)
;(get-model)
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(push)
(assert (and (> (* a a) 3) (= (+ (* b b b) (* b c)) 3.0)))
(check-sat)
(check-sat-using qfnra-nlsat) ; force using nonlinear solver for nonlinear real arithimetic (coerce integers to reals)
(get-model)
(pop)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)
同样，如果仅将(declare-const a Int)更改为(declare-const a Real)，则默认情况下它将选择可以处理此问题的正确求解器.因此，是的，从本质上讲，这与选择的求解器有关，而求解器的选择部分取决于基础术语的种类.
相关问答:将非线性实数与线性Int组合
I am just starting to use Z3 (v4.4.0), and I wanted to try one of the tutorial examples :
(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
As said, the second example fails with "unknown", and by increasing the verbose level (to 3) I think I understand why : some problem with the simplifying process, then the tactic fails. In order to have a better idea of the problem (and a shorter output), I decided to remove the first part of the code to test only the failed part :
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
But magically, now I get "sat". I am not sure about how Z3 chooses its tactic when it is about non linear arithmetic, but can the problem be from Z3 choosing a tactic for the first formula that is useless for the second one ?
Thanks in advance
The second encoding is not equivalent to the first, hence the different behavior. The second encoding does not include the constraint (assert (> (* a a) 3)), so Z3 can find it is satisfiable that b^3 + b*c = 3 for some choice of reals b and c. However, when it has the constraint that a^2 > 3 for some integer a, it fails to find it's satisfiable, even though the two assertions are independent from one another.
For this problem, it's essentially that Z3 by default will not use the nonlinear real arithmetic solver (which is complete) when it encounters reals mixed with integers. Here's an example of how to force it using qfnra-nlsat (rise4fun link: http://rise4fun.com/Z3/KDRP ):
(declare-const a Int)
;(assert (> (* a a) 3))
;(check-sat)
;(get-model)
(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(push)
(assert (and (> (* a a) 3) (= (+ (* b b b) (* b c)) 3.0)))
(check-sat)
(check-sat-using qfnra-nlsat) ; force using nonlinear solver for nonlinear real arithimetic (coerce integers to reals)
(get-model)
(pop)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)
Likewise, if you just change (declare-const a Int) to (declare-const a Real), it will by default pick the correct solver that can handle this. So yes, in essence this has to do with what solver is getting picked, which is determined in part by the sorts of the underlying terms.
Related Q/A: Combining nonlinear Real with linear Int
这篇关于Z3:非线性算法的奇怪行为的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
