代码之家 › 专栏 › 技术社区 › S. L.

Z3返回模型不可用

S. L. · 技术社区 · 6 年前

如果可能的话,我想对我的代码提出第二个意见。

问题的约束条件是:

a,b,c,d,e,f 是非零整数
s1 = [a,b,c] 和 s2 = [d,e,f] 是集
和 s1_i + s2_j 对于 i,j = 0..2 必须是一个完美的正方形

我不明白为什么,但我的代码返回模型不可用。此外,在评论以下几行时:

(assert (and (> sqrtx4 1) (= x4 (* sqrtx4 sqrtx4))))
(assert (and (> sqrtx5 1) (= x5 (* sqrtx5 sqrtx5))))
(assert (and (> sqrtx6 1) (= x6 (* sqrtx6 sqrtx6))))

(assert (and (> sqrtx7 1) (= x7 (* sqrtx7 sqrtx7))))
(assert (and (> sqrtx8 1) (= x8 (* sqrtx8 sqrtx8))))
(assert (and (> sqrtx9 1) (= x9 (* sqrtx9 sqrtx9))))

d、e、f的值为负值。没有约束要求他们这样做。我想知道是否有一些隐藏的限制潜入和混乱的模型。

有效的预期解决方案是:

a = 3
b = 168
c = 483
d = 1
e = 193
f = 673

编辑插入 (assert (= a 3)) 和 (assert (= b 168)) 结果解算器找到正确的值。这只会让我更加困惑。

完整代码:

(declare-fun sqrtx1 () Int)
(declare-fun sqrtx2 () Int)
(declare-fun sqrtx3 () Int)
(declare-fun sqrtx4 () Int)
(declare-fun sqrtx5 () Int)
(declare-fun sqrtx6 () Int)
(declare-fun sqrtx7 () Int)
(declare-fun sqrtx8 () Int)
(declare-fun sqrtx9 () Int)

(declare-fun a     () Int)
(declare-fun b     () Int)
(declare-fun c     () Int)
(declare-fun d     () Int)
(declare-fun e     () Int)
(declare-fun f     () Int)

(declare-fun x1     () Int)
(declare-fun x2     () Int)
(declare-fun x3     () Int)
(declare-fun x4     () Int)
(declare-fun x5     () Int)
(declare-fun x6     () Int)
(declare-fun x7     () Int)
(declare-fun x8     () Int)
(declare-fun x9     () Int)


;all numbers are non-zero integers
(assert (not (= a 0)))
(assert (not (= b 0)))
(assert (not (= c 0)))
(assert (not (= d 0)))
(assert (not (= e 0)))
(assert (not (= f 0)))

;both arrays need to be sets
(assert (not (= a b)))
(assert (not (= a c)))
(assert (not (= b c)))

(assert (not (= d e)))
(assert (not (= d f)))
(assert (not (= e f)))



(assert (and (> sqrtx1 1) (= x1 (* sqrtx1 sqrtx1))))
(assert (and (> sqrtx2 1) (= x2 (* sqrtx2 sqrtx2))))
(assert (and (> sqrtx3 1) (= x3 (* sqrtx3 sqrtx3))))


(assert (and (> sqrtx4 1) (= x4 (* sqrtx4 sqrtx4))))
(assert (and (> sqrtx5 1) (= x5 (* sqrtx5 sqrtx5))))
(assert (and (> sqrtx6 1) (= x6 (* sqrtx6 sqrtx6))))

(assert (and (> sqrtx7 1) (= x7 (* sqrtx7 sqrtx7))))
(assert (and (> sqrtx8 1) (= x8 (* sqrtx8 sqrtx8))))
(assert (and (> sqrtx9 1) (= x9 (* sqrtx9 sqrtx9))))

;all combinations of sums need to be squared
(assert (= (+ a d) x1))
(assert (= (+ a e) x2))
(assert (= (+ a f) x3)) 

(assert (= (+ b d) x4))
(assert (= (+ b e) x5))
(assert (= (+ b f) x6))

(assert (= (+ c d) x7))
(assert (= (+ c e) x8))
(assert (= (+ c f) x9))


(check-sat-using (then simplify solve-eqs smt))
(get-model)
(get-value (a))
(get-value (b))
(get-value (c))
(get-value (d))
(get-value (e))
(get-value (f))

1 回复 | 直到 6 年前

alias 6 年前

非线性整数算法是不可判定的。这意味着没有决策过程可以决定任意非线性整数约束是否满足。这就是Z3在回答你的问题时告诉你的。

当然,这并不意味着个别案件不能得到解决。Z3有一定的策略,它适用于解决这类公式,但它在本质上是有限的,它可以处理。你的问题属于这一类:Z3无法解决的问题。

Z3有一个专用的NRA(非线性实数算法)策略,你可以利用。它本质上把所有变量都看作实数,解决了问题(非线性实数算法是可判定的,Z3可以找到所有代数实数解),然后检查结果是否是整数。如果不是,它会尝试另一种解决方案。有时这种策略可以处理非线性整数问题,如果您恰巧找到了正确的解决方案。您可以使用以下方法触发它:

(check-sat-using qfnra)

不幸的是,在我允许它运行的时候,它不能解决您的特定问题。(超过10分钟)它不太可能达到正确的解决方案。

你真的没有很多选择。SMT解算器并不能很好地解决非线性整数问题。事实上,正如我前面提到的,由于不确定性,没有一个工具可以处理任意的非线性整数问题;但是一些工具比其他工具更好,这取决于它们使用的算法。

当你告诉Z3什么 a 和 b 是的,你基本上消除了大部分的非线性,剩下的变得容易处理。你可能会找到一系列的策略来解决你原来的问题,但是这些技巧在实践中是非常脆弱的,而且不容易被发现;因为你本质上是在搜索中引入启发式方法,而你对它的行为没有太多的控制。

旁注:你的脚本可以稍作改进。要表示一组数字都不同,请使用不同的谓词:

(assert (distinct (a b c)))
(assert (distinct (d e f)))