问题描述
我试图通过将以下内容放在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环境中对它们进行建模是正确的选择。