了解Z3在量化的LIA公式上的低性能

Question

我遇到了以下公式，该公式需要Z3几分钟才能解决：

(set-logic LIA)
(assert
    (forall ((f Int))
        (exists ((a Int) (b Int))
            (= (+ (* 17 a) (* 19 b)) f)
        )
    )
)

(check-sat)
(exit)

我已经阅读了纸记录Z3用来决定LIA的方法，但是，我看不出Z3为何在给定公式中挣扎。你能解释一下吗？

Answer 1

量词很难，嵌套的量词更难。在任何给定的SMT溶剂中，内部发生了什么，真的很难猜测。很遗憾。除非您投资研究其内部设备，否则它们是或多或少的黑盒子。关于所使用技术的一本好书是Kroening和Strichman的决策程序 。您可能需要阅读该书，其中还包含进一步的参考。

请注意，当SMT求解器“试图找到模型”而不是试图证明事物时，他们会做得更好，因此通常会要求否定定理要满足。然后取消结果表明理论。将此翻译成您的问题，一个人会得到：

(set-logic LIA)
(declare-fun f () Int)
(assert
  (forall ((a Int) (b Int))
      (distinct (+ (* 17 a) (* 19 b)) f)
  )
)

(check-sat)
(exit)

不幸的是，Z3在此形式上花费更长的时间；这让我感到惊讶。 （我已经期望至少相同的性能。）但是 yices 立即解决！ （为了进行比较，CVC5似乎也永远在上面运行，谁知道原因。）因此，如果您遇到这种问题，您可能想尝试YICES。

Yices在此方面表现良好的事实，而Z3并不意味着Z3可能缺少某些启发式，或者是Yices拥有的重写。您可能需要在。不是作为错误，而是作为好奇心，为什么YICES表现更好。我敢肯定，即使开发人员选择不做任何使Z3在此问题上更快的事情，他们也会很高兴听到有关此问题的消息。