将变量约束在数组中

Question

我正在解决的问题涉及确保某些变量是完美的正方形。

据我了解，z3 中还没有对 sqrt 的原生支持。我的想法是简单地使用第一个说 300 个方格的数组并检查是否包含变量。我该怎么办？

坦率地说，由于我对 z3 不是非常精通，因此对于如何解决问题可能会有更好的建议，对任何事情都开放！

Answer 1

如果不确切知道您要做什么，很难在这里提出好的建议。但是，也许您不需要sqrt？如果你想要的只是完全平方的数字，那么你可以反过来：

(declare-fun sqrtx () Int)
(declare-fun x     () Int)

; this will make sure x is a perfect square:
(assert (and (>= sqrtx 0) (= x (* sqrtx sqrtx))))

; make it interesting:
(assert (> x 10))

(check-sat)
(get-value (x sqrtx))

打印出来：

sat
((x 16)
 (sqrtx 4))

本质上，对于您想要的每个“完美正方形”，您都可以声明一个幽灵变量并断言所需的关系。

请注意，这会导致非线性（因为您将两个符号值相乘），因此求解器可能很难处理您的所有约束。但是在没有看到你真正想要做什么的情况下，我认为这将是获得完美平方并与之推理的最简单方法。