z3在处理非线性实数运算时总能给出结果吗 [英] Can z3 always give result when handling nonlinear real arithmetic

问题描述

我有一个问题需要解决一组非线性多项式约束.在处理非线性实数算术时，z3 是否总能给出结果(sat 或 unsat).结果也合理吗?

解决方案

是的，假设 (1) 资源可用，并且 (2) 你只使用真正的约束使得 nlsat使用了策略，正如我上次检查的那样，它没有与其他求解器完全集成，有关更多详细信息，请参阅以下问题/答案.这是一个说明这一点的简单示例(至少在默认情况下，rise4fun 链接:http://rise4fun.com/Z3/SRZ8 ):

(declare-fun x () Real)(declare-fun y () Real)(declare-fun z () Real)(断言 (>= (* 2 (^ x 2)) (* y z)))(断言 (> x 100))(断言 (< y 0))(断言 (< z 0))(断言 (> (^ y 2) 1234))(断言 (< (^ z 3) -25))(检查周六)；坐(获取模型)(declare-fun b() Int)(断言 (> b x))(检查周六)；未知

• Z3 定理证明器:勾股定理(非线性算法)

• 混合实数和位向量>

• z3 为没有量词的断言生成未知

• z3 实数存在论

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

• Z3 支持非线性算术

• 编码返回未知"

对于增量问题，可以使用 nlsat 进行增量求解，但在这个简单的示例中应用了标准方法(rise4fun 链接:http://rise4fun.com/Z3/Ce1F 并查看:Z3 中的软/硬约束 ) 有一个未知数，尽管进行了模型分配，因此它可能对您的目的有用.如果没有，您可以尝试push/pop:使用push命令在Z3中增量求解

(set-option :produce-unsat-cores true)(设置选项:生产模型真)(declare-const p1 Bool)(declare-const p2 Bool)(declare-const p3 Bool)(declare-const p4 Bool)(declare-const p5 Bool)(declare-const p6 Bool)(declare-const p7 Bool)(declare-fun x () Real)(declare-fun y () Real)(declare-fun z () Real)(断言 (=> p1 (>= (* 2 (^ x 2)) (* y z))))(断言(=> p2(> x 100)))(断言(=> p3( p4( p5 (> (^ y 2) 1234)))(断言(=> p6(<(^ z 3)-25)))(断言(=> p7( b x))(检查周六)；未知

I have a problem required to solve a set of nonlinear polynomial constraints. Can z3 always give a result (sat or unsat) when handling nonlinear real arithmetic. Is the result also sound?

解决方案

Yes, it is complete assuming (1) availability of resources, and (2) you only use real constraints so that the nlsat tactic is used, as the last I checked, it wasn't full integrated with the other solvers, see the below questions/answers for more details. Here's a simple example illustrating this (at least by default, rise4fun link: http://rise4fun.com/Z3/SRZ8 ):

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (>= (* 2 (^ x 2)) (* y z)))
(assert (> x 100))
(assert (< y 0))
(assert (< z 0))
(assert (> (^ y 2) 1234))
(assert (< (^ z 3) -25))
(check-sat) ; sat
(get-model)

(declare-fun b () Int)
(assert (> b x))
(check-sat) ; unknown

• Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)

• mixing reals and bit-vectors

• z3 produces unknown for assertions without quantifiers

• z3 existential theory of the reals

• Combining nonlinear Real with linear Int

• Z3 support for nonlinear arithmetic

• Encoding returns "unknown"

For the incremental question, it may be possible to use nlsat with incremental solving, but in this simple example applying a standard method (rise4fun link: http://rise4fun.com/Z3/Ce1F and see: Soft/Hard constraints in Z3 ) there is an unknown, although a model assignment is made, so it may be useful for your purposes. If not, you can try push/pop: Incremental solving in Z3 using push command

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const p5 Bool)
(declare-const p6 Bool)
(declare-const p7 Bool)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (=> p1 (>= (* 2 (^ x 2)) (* y z))))
(assert (=> p2 (> x 100)))
(assert (=> p3 (< y 0)))
(assert (=> p4 (< z 0)))
(assert (=> p5 (> (^ y 2) 1234)))
(assert (=> p6 (< (^ z 3) -25)))
(assert (=> p7 (< x 50)))
(check-sat p1 p2 p3 p4 p5 p6 p7) ; unsat
(get-unsat-core) ; (p2 p7)

(check-sat p1 p2 p3 p4 p5 p6) ; unknown, removed one of the unsat core clauses
(get-model)

(declare-fun b () Int)
(assert (> b x))
(check-sat) ; unknown

这篇关于z3在处理非线性实数运算时总能给出结果吗的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！