为什么Z3在某些条件下使用均匀信息会遇到麻烦

Question

我有以下查询可行的查询：

(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod c 2))) ; c is even
(assert (= b (div c 2))) ; b = c/2
(assert (not (= c (* 2 b)))) ; c != 2*b
(check-sat)

正如预期的那样，我会解开。但是，如果我用(n *(n 1((替换c，我会变得未知(由5068D2083DC0609801F572A0E3D14DF753D36A03构建的本地Z3，大约4.5.1(或超时(在http:///rise4fun.com/p.3(：

上

(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod (* n (+ 1 n)) 2)))
(assert (= b (div (* n (+ 1 n)) 2)))
(assert (not (= (* n (+ 1 n)) (* 2 b))))
(check-sat)

任何想法，为什么在一种情况下它会弄清楚它，但不在另一个情况下？

谢谢！〜DIMO

Answer 1

当您放入n * (n+1)时，问题变成非线性。(非线性是指您乘以非恒定剂量。(

在这种情况下，默认求解器不太可能产生结果，因为决策算法仅适用于逻辑的线性片段。本质上，您受到启发式的摆布：如果他们能解决您的问题，那就太好了；如果没有，您将获得一个unknown的答案。

话虽如此，您可以使用"策略"来指导求解器。在这种情况下，以下情况似乎有效：

(check-sat-using (and-then qfnra-nlsat smt))

这样，z3成功返回了查询的 unsat。

有关详细信息，请参见http://rise4fun.com/z3/tutorial/strategies。知道哪种策略可以解决哪个问题是一门艺术，但是如果您阅读了本教程，您可以很好地了解如何尝试。