时间戳

首页 > 解决方案 > Z3求解器无法求解2 ^ x = 4是否正常？

z3 - Z3求解器无法求解2 ^ x = 4是否正常？

问题描述

我试图通过在 Z3 网站上放置以下内容来使用 Z3 解决 2^x=4： https ://rise4fun.com/z3/tutorial 。

(declare-const x Real) 
(declare-const y Real) 
(declare-const z Real) 
(assert (=(^ 2 x) 4)) 
(check-sat) 
(get-model)

Z3出品

unknown
(model 
)

我在滥用 Z3 吗？

标签： z3smtsatisfiability

解决方案

涉及指数的问题通常超出 z3 或通用 SMT 求解器的范围。这并不意味着他们无法解决它们：实数理论是可判定的。但是他们可能没有正确的“启发式”来回答每个涉及指数的查询作为sat/ unsat。您可以在 stack-overflow 中搜索 、 等关键字nnf，non-linear以查看有关涉及此类困难术语的查询的大量问题。

话虽如此，有一个单独的研究方向称为 delta-satisfiability 可以在很大程度上帮助解决这些问题。请注意，增量可满足性与常规可满足性不同。这意味着该公式要么是可满足的，要么是它的增量扰动。最突出的此类求解器是dReal，您可以在此处阅读所有相关信息：http: //dreal.github.io/

对于您的查询，dReal说：

[urfa]~/qq>dreal a.smt2
delta-sat with delta = 0.001
(model
  (define-fun x () Real [2, 2])
  (define-fun y () Real [-0.0005, 0.0005])
  (define-fun z () Real [-0.0005, 0.0005])
)

（您实际上并没有在查询中使用y和z，因此您可以忽略这些输出。）

如您所见，dReal确定x必须在范围内[2, 2]，即它必须是2。但它也说delta-sat with delta = 0.001：这意味着它确保了该因素的正确性。（您可以自己调整因子，使其任意小，但不为零。）当您遇到物理系统产生的问题时，delta-sat 是在 SMT 世界中对其进行建模的正确选择。

推荐阅读