Z3求解器不能求解2 ^ x = 4的那正常吗？

如何解决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吗？

解决方法

涉及指数的问题通常是z3或通用SMT求解器无法解决的。这并不意味着他们无法解决它们：实在理论是可以决定的。但是他们可能没有正确的“试探法”来回答每个涉及sat / unsat指数的查询。您可以在堆栈溢出中搜索nnf，non-linear等关键字，以查看有关涉及此类困难术语的查询的过多问题。

话虽这么说，但有另一项研究称为德尔塔可满足性，可以在很大程度上帮助解决此类问题。请注意，与常规满意度相比，Delta满意度不同。这意味着该公式是可满足的，或者是它的增量扰动。最杰出的求解器是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：这意味着它已确保该因素内的正确性。（您可以自己调整因子，使其任意小，但不为零。）当物理系统产生问题时，在SMT环境中对它们进行建模是正确的选择。