Z3 中有理数的线性问题是否可判定？

Question

我正在 Z3 中处理关于有理数的线性问题。要使用 Z3 我需要 SBV.

我提出的一个问题示例是：

import Data.SBV

solution1 = do
  x <- sRational "x"
  w <- sRational "w"
  constrain $ x.< w
  constrain $ x + 2*w .>=0 .|| x .== 1

我的问题是：

这类问题是可判定的吗？我找不到可判定理论列表或判断理论是否可判定的方法。我找到的最接近的是 this。关于实数的理论是可判定的，但对于有理数来说也是如此吗？直觉告诉我是的，但我还没有找到让我确信的资料。

提前致谢

Answer 1

我想当且仅当整数解决方案存在于适当缩放的约束集合时，才会存在合理的解决方案。例如，x=1/2(=5/10), w=3/5(=6/10) 是您的示例问题的解决方案。将您的问题缩放 10，我们有等效的约束集：

10*x < 10*w
(10*x + 20*w >= 0) || (10*x == 10)

写作x'=10*x和w'=10*w，这意味着x'=5, w'=6是一个整数解：

x' < w'
(x' + w' >= 0) || (x' == 10)

Presburger 著名地表明 first-order 逻辑加上整数和加法是可判定的。（乘以常数也是允许的，因为它可以扩展为加法——例如 3*x 是 x+x+x。）

我想剩下的唯一技巧就是证明可以在尚未解决问题的情况下选择要使用的缩放比例。我没有想到任何明显的事情发生，但这应该是可行的似乎是合理的。例如，如果您采用约束集中所有非零分子和分母的乘积，您可以证明以该乘积作为其分母的有理数集与完整的有理数集无法区分。（如果是这样，您可以查看证明，看看它是否仍然适用于较小的分母。）

我不是 z3 专家，所以我不能谈论这如何转化为该工具是否特别合适，但在我看来，有可能创建一个合适的工具。

Answer 2

SBV 使用标准的“两个整数”思想对有理数建模；也就是说，它将分子和分母分别表示为整数。这意味着如果您添加两个符号有理数，您将在整数上有一个 non-linear 项。因此，理论上，问题将出在 semi-decidable 片段中。也就是说，即使您将乘法限制为具体标量，符号有理数的加法也会在整数上产生 non-linear 项。

话虽如此，我使用有理数时运气不错；其中 z3 能够毫不费力地解决大多数感兴趣的问题。如果它被证明是一个问题，你应该切换到 SReal 类型（即代数实数），z3 有一个决策程序。但当然，你得到的模型现在可以包括代数实数，例如 square-root-of-2 等（即任何具有整数系数的多项式的根。）

旁注如果您的问题允许 delta-sat（即扰动的可满足性），您应该研究 dReal (http://dreal.github.io)，SBV还支持作为后端求解器。但也许这不是你想要的。

理论笔记

严格来说，有理数上的线性算术是可判定的；请参阅 https://www.cs.ox.ac.uk/people/james.worrell/lecture15-2015.pdf 的第 3 节以获取证明。但是，SMT 求解器不支持有理数out-of-the-box；和 SBV（正如我上面提到的），使用两个符号整数来表示有理数。因此，添加两个有理数将导致两个符号整数相乘，从而使您脱离可判定片段。当然，在实践中，即使存在 non-linear 项，求解器也非常善于提出解决方案；只是你不能总是得到保证。因此，对您的问题的更严格的回答是虽然有理数的线性算术是可判定的，但 SBV 使用的转换将问题置于 non-linear 整数算术域中，因此无法保证可判定性。无论如何，SMTLib 不附带有理数理论，因此当谈到第一个 class 对它们的支持时，您有点 out-of-luck。

Z3 中有理数的线性问题是否可判定？

Are linear problems on rational numbers decidable in Z3?

haskell

z3

smt

decidable

sbv

理论笔记