Z3 返回模型不可用 [英] Z3 returns model not available

问题描述

如果可能，我想对我的代码有第二意见.

If possible I'd like a second opinion on my code.

问题的约束是:

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

• a,b,c,d,e,f are non-zero integers
• s1 = [a,b,c] and s2 = [d,e,f] are sets
• The sum s1_i + s2_j for i,j = 0..2 has to be a perfect square

我不明白为什么我的代码返回模型不可用.此外，当注释掉以下几行时:

I don't understand why but my code returns model not available. Moreover, when commenting out the following lines:

(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 的值为负.没有任何限制要求他们这样做.我想知道是否有一些隐藏的约束潜入并弄乱了模型.

The values for d, e, f are negative. There is no constraint that requires them to do so. I'm wondering if perhaps there are some hidden constraints that sneaked in and mess up the model.

一个有效的预期解决方案是:

A valid expected solution would be:

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

编辑:插入 (assert (= a 3)) 和 (assert (= b 168)) 导致求解器找到正确的价值观.这只会让我更加困惑.

Edit: inserting (assert (= a 3)) and (assert (= b 168)) results in the solver finding the correct values. This only puzzles me further.

完整代码:

(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))

推荐答案

非线性整数算法是不可判定的.这意味着没有决策程序可以决定任意非线性整数约束是可满足的.这就是当 z3 说未知"作为您查询的答案时告诉您的内容.

Nonlinear integer arithmetic is undecidable. This means that there is no decision procedure that can decide arbitrary non-linear integer constraints to be satisfiable. This is what z3 is telling you when it says "unknown" as the answer your query.

这当然并不意味着个别案例无法回答.Z3 有一定的策略来解决此类公式，但它的处理能力本质上是有限的.您的问题属于这一类:Z3 无法解决的问题.

This, of course, does not mean that individual cases cannot be answered. Z3 has certain tactics it applies to solve such formulas, but it is inherently limited in what it can handle. Your problem falls into that category: One that Z3 is just not capable of solving.

Z3 具有您可以使用的专用 NRA(非线性实数算法)策略.它本质上将所有变量都当作实数，解决问题(非线性实数算术是可判定的，z3 可以找到所有代数实数解)，然后检查结果是否实际上是整数.如果不是，它会在实数上尝试另一种解决方案.有时，如果您碰巧找到正确的解决方案，这种策略可以处理非线性整数问题.您可以使用以下方法触发它:

Z3 has a dedicated NRA (non-linear real arithmetic) tactic that you can utilize. It essentially treats all variables as reals, solves the problem (nonlinear real arithmetic is decidable and z3 can find all algebraic real solutions), and then checks if the results are actually integer. If not, it tries another solution over the reals. Sometimes this tactic can handle non-linear integer problems, if you happen to hit the right solution. You can trigger it using:

(check-sat-using qfnra)

不幸的是，在我允许它运行的时间内，它并没有解决您的特定问题.(超过 10 分钟.)它不太可能找到正确的解决方案.

Unfortunately it doesn't solve your particular problem in the time I allowed it to run. (More than 10 minutes.) It's unlikely it'll ever hit the right solution.

你在这里真的没有很多选择.SMT 求解器不太适合非线性整数问题.事实上，正如我上面提到的，由于不可判定性，没有任何工具可以处理任意非线性整数问题；但有些工具的性能要好于其他工具，这取决于它们使用的算法.

You really don't have many options here. SMT solvers are just not a good fit for nonlinear integer problems. In fact, as I alluded to above, there is no tool that can handle arbitrary nonlinear integer problems due to undecidability; but some tools fare better than others depending on the algorithms they use.

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

When you tell z3 what a and b are, you are essentially taking away much of the non-linearity, and the rest becomes easy to handle. It is possible that you can find a sequence of tactics to apply that solves your original, but such tricks are very brittle in practice and not easily discovered; as you are essentially introducing heuristics into the search and you don't have much control over how that behaves.

旁注:您的脚本可以稍微改进.要表示一堆数字都不同，请使用不同的谓词:

Side note: Your script can be improved slightly. To express that a bunch of numbers are all different, use the distinct predicate:

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

这篇关于Z3 返回模型不可用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！