0

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?

Dingbao Xie
  • 716
  • 9
  • 21
  • There's no guarantee that a solution exists with non-linear systems. – duffymo Jan 22 '14 at 13:32
  • Duffymo: non polynomial real arithmetic is decidable (and in fact admits quantifier elimination). What you are referring to is perhaps non-linear integer arithmetic, which is undecidable. – David Monniaux Mar 01 '14 at 11:18

1 Answers1

1

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
Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17
  • Is the result also sound? Another question is that is it possible to solve problems in a incremental way when using nlsat tactic? – Dingbao Xie Jan 23 '14 at 02:38
  • Yes, generally speaking Z3 is sound modulo bugs in the implementation. In some cases, you may be able to mix the propositions needed by one of the usual incremental method (see: http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3 ) with the nonlinear constraints to be useful, but it's unsat/unknown in my example, but there is a model assignment, so it may or may not be useful for your purposes. I've updated the answer to give an example of this, but you may just want to use push/pop: http://stackoverflow.com/questions/18269016/incremental-solving-in-z3-using-push-command – Taylor T. Johnson Jan 23 '14 at 04:35
  • It seems that z3 also supports unsat core extraction when handling nonlinear real arithmetic. I know that it's very expensive to do the unsat core extraction. Can you tell me how large problems z3 can handle when it is needed to extract an unsat core in nonlinear real arithmetic? – Dingbao Xie Jan 23 '14 at 05:50