对于这个非线性整数算术示例，为什么 Z3 返回 unknown ? [英] Why does Z3 return unknown for this nonlinear integer arithmetic example?

问题描述

我有一个非线性整数算术的简单示例，即对勾股数三元组的搜索.根据我在相关问题中读到的内容(见下文)，我希望 Z3 找到解决此问题的方法，但它返回未知".这是 SMT-LIB v2 中的示例:

I have a simple example in nonlinear integer arithmetic, namely a search for Pythagorean triples. Based on what I read in related questions (see below), I'd expect Z3 to find a solution to this problem, but it returns 'unknown'. Here is the example in SMT-LIB v2:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun xSquared () Int)
(declare-fun ySquared () Int)
(declare-fun zSquared () Int)
(declare-fun xSquaredPlusYSquared () Int)

(assert (= xSquared (* x x)))
(assert (= ySquared (* y y)))
(assert (= zSquared (* z z)))
(assert (= xSquaredPlusYSquared (+ xSquared ySquared)))

(assert (and (> x 0) (> y 0) (> z 0) (= xSquaredPlusYSquared zSquared)))

(check-sat)

(exit)

<小时>

有几个相关的问题，最值得注意的是:

---

There are a few related questions, most notably:

• Z3 如何处理非线性整数算法?

需要帮助理解等式

结合非线性实数和线性整数

Z3 支持非线性算术

z3 在处理非线性实数算术方面的限制

推荐答案

Z3 似乎不会尝试通过位爆破来寻找解决方案，除非变量具有有限范围.将 (check-sat) 替换为以下命令将找到解决方案:

It seems that Z3 won't attempt finding a solution by bit-blasting unless variables have a finite range. Replacing (check-sat) with the following command will find the solution:

(check-sat-using (then (using-params add-bounds :add-bound-lower -100 :add-bound-upper 100) smt))

或者，可以添加 assert 语句，强制每个变量具有一定的范围.

Alternatively, one can add assert statements forcing each variable to have some finite range.

这篇关于对于这个非线性整数算术示例，为什么 Z3 返回 unknown ?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！