英文:
Unknown answer for simple SMT-LIB expression
问题
我对SMT求解是新手。下面的表达式是一个非常简单的示例。
行4和5将变量z的可能值限制为零或一。接下来的步骤是计算2**0 - 1或2**1 - 1。结果是，变量K可以是零或一。
然而，第8行的可满足性显示为未知。在我第一次使用SMT表达式进行约束求解的经验中，我觉得奇怪的是求解器不能解决这个简单的线性表达式。如果我取消注释第6行，结果会变成“可满足”。但是，取消注释这一行不是期望的，因为所有未知变量应该由用户提供。
所以，我的问题是：给定的表达式是否无法解决？还是可以通过某种方式将它们转化为另一种形式来解决？
谢谢
我编写了一个简单的示例，并看到了不希望的结果。因此，我想请教专家，这个结果是否是预期的，或者是否可以通过重构来解决。
英文:
I'm new to SMT solving. The expression below is a very simple example.
1: (declare-const x Int)
2: (declare-const z Int)
3: (declare-const k Int)
4: (assert (= z (* x x))) ; z = x*x
5: (assert (<= z 1)) ; z <= 1, where z should be either 0 or 1
6: ; (assert (= x 1))
7: (assert (= k (- (^ 2 z) 1))) ; k = 2**z - 1
8: (check-sat)
Lines 4 and 5 narrow down the possible values of the variable z to either zero or one. The next step is to calculate 2**0 - 1 or 2**1 - 1. As a result, the variable K can be either zero or one.
However, the satisfiability in line 8 displays unknown. In my first experience of constraint solving using SMT expressions, it seems strange to me that the solver cannot solve this simple linear expression. If I uncomment line 6, the result changes to sat. However, uncommenting this line is not desired because all unknown variables should be provided by the user.
So, my question is: Can the given expressions not be resolved? Or can they be resolved by transforming them into another form somehow?
Thank you
I've written a simple example and saw the undesired result. So, I'd like to ask to experts whether this result is expected or can be resolved by refactoring.
答案1
得分: 0
这里有两个问题。首先是幂运算符创建了一个实数项。（考虑一下，例如，2^(-1)。结果不是整数，即使参数是整数。）因此，你应该明确进行类型转换：
(assert (= k (- (to_int (^ 2 z)) 1))) ; k = 2**z - 1
如果你这样做，你会看到 z3 返回了 sat 作为答案。（很难猜测为什么 z3 不能聪明地推导出这一点，可能是某些“触发器”在没有类型转换的情况下未能触发。但在没有分析 z3 代码本身的情况下很难说。）
不幸的是，第二个问题更难处理。对于 SMT 求解器来说，指数运算很困难：它们创建高度非线性的项，而非线性整数算术不仅是不可判定的，而且处理它的现有算法（例如，归约为增量位向量）也必然非常昂贵。因此，根据你的其他约束条件，你可能仍然会得到 unknown 作为答案。
但最好针对每个问题分别处理。对于每个问题，通常都有一种替代的编码方法来获取答案，尽管在存在非线性项时不应期望完全的一键解决方案。
英文:
There are two issues here. The first is that power operator creates a real-valued term. (Think of, for instance, 2^(-1). The result isn't an integer even though the arguments are.) So, you should explicitly cast:
(assert (= k (- (to_int (^ 2 z)) 1))) ; k = 2**z - 1
If you do this, you'll see that z3 answers your query as sat. (It's hard to guess why z3 isn't smart enough to deduce this, probably some "trigger" fails to fire without the cast. But hard to tell without analyzing the z3 code itself.)
The second issue, unfortunately, is harder to deal with. Exponentiation is difficult for SMT solvers: They create highly non-linear terms, and non-linear integer arithmetic is not only undecidable, the existing algorithms that deal with it (reduction to incremental bit-vectors, for instance) are necessarily very expensive. So, depending on your other constraints you might still get unknown as an answer.
But it's best to deal with each problem on its own. For each problem, there's usually an alternative way to code it to get answers, though you shouldn't expect complete push-button solutions when non-linear terms are present.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论