无法解释简单的调整如何导致 "unknown" Z3 结果

Question

我正在学习 Z3。我在使用一些简单的 "isPrime" 函数时偶然发现了一些难以理解的行为。一个看似 "simpler" 的内联公式，(> q 1)，导致 "unknown"，而不是一个更 "complex" 定义有趣的（宏），(isPrime q)，导致一个快速的解决方案，即使 (isPrime q) 包含 (> q 1)。 http://rise4fun.com/Z3/slg2D.

(define-fun isPrime ((x Int)) Bool
  (and (> x 1) (not (exists ((z Int) (y Int)) (and (not (= y x)) (and (not (= z x)) (and (> y 1) (> z 1) (= x (* y z)))))))))
(declare-const q Int)
(declare-const r Int)
(assert (and
  ;with this the '+ 2' variation is sat: 5, 3
  ;(isPrime q)
  (> q 1)
  (> r 1)
  ;always answers sat: 2, 2
  ;(isPrime (+ (* q r) 1))
  ;unknown
  (isPrime (+ (* q r) 2))
))
(check-sat)
(get-model)

Answer 1

量化逻辑是一种高级功能，您应该了解 Z3 如何求解这些公式，这将使您对 Z3 的期望有一个看法。以我的微薄经验，用量词求解公式是一门精致的艺术。对你来说显而易见的事情，对 Z3 来说可能并不明显。

您有一个 forall 量词（您将其写为 not exists），Z3 将尝试满足该量词。我猜 Z3 正在选择一些 q 和 r，然后检查 isPrime 是否成立，否则它会尝试使用新的一对，依此类推。如果Z3没有做出正确的选择，它可能需要一段时间才能找到这样的q和r，所以也许你应该给它更多的时间（在rise4fun上解决问题有超时）。

另一种方法是帮助 Z3 多一点。例如，让它知道 z 和 y 小于 x。通过这种方式，您可以为这些变量提供下限和上限。

(define-fun isPrime ((x Int)) Bool
   (and (> x 1) (not (exists ((z Int) (y Int)) (and (< y x) (and (< z x) (and (> y 1) (> z 1) (= x (* y z)))))))))

This 适合我。

更新

参考文献：

Leonardo de Moura 关于 SAT/SMT 2012 年暑期学校的演讲 (https://es-static.fbk.eu/events/satsmtschool12/)
Z3 教程，量词 (http://rise4fun.com/Z3/tutorial/guide)
通用 Z3 教程（http://research.microsoft.com/en-us/um/redmond/projects/z3/mbqi-tutorial/main.html）

无法解释简单的调整如何导致 "unknown" Z3 结果

Can't explain how a simple tweak leads to "unknown" Z3 result

z3