CODEWITHSUNDEEP
z3
Dingbao Xie
Dingbao Xie

Reputation: 736

Can z3 always give result when handling nonlinear real arithmetic

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?

Upvotes: 0

Views: 800

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

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

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

Upvotes: 1

Related Questions