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

【问题标题】：Understanding Z3's low performance on a quantified LIA formula了解 Z3 在量化 LIA 公式上的低性能
【发布时间】：2022-08-08 10:51:16
【问题描述】：

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

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

(check-sat)
(exit)

我已经阅读了paper 记录了 Z3 用来决定 LIA 的方法，但是，我不明白为什么 Z3 会在给定的公式上挣扎。你能解释一下吗？

标签： z3 smt

【解决方案1】：

量词很难，嵌套的量词更难。很难猜测任何给定的 SMT 求解器内部发生了什么。很遗憾。它们或多或少是黑匣子，除非你投资研究它们的内部结构。一本关于所用技术的好书是 Kroening 和 Strichman 的 Decision Procedures，其中有一整章是关于线性算术的。您可能想通读那本书，其中还包含更多参考资料。

请注意，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 的重写。您可能希望通过https://github.com/Z3Prover/z3/issues 报告此差异。不是作为一个错误，而是作为一个好奇心，为什么 yices 表现得更好。我相信开发人员会很高兴听到这个消息，即使他们选择不做任何事情来让 z3 在这个问题上运行得更快。

【讨论】：

根据 yices 网站上链接的paper，求解器包含直接针对具有“exists-forall”结构的问题的启发式算法，解释了为什么 yices 能够求解给定公式。我还阅读了描述 z3 如何接近线性算术的paper，但是鉴于有问题的公式，我没有看到 z3 方法的哪一部分有问题，因此，我尝试询问 SO。