How to optimize a piece of code in Z3? (PI_NON_NES

问题:

I have a code in z3 which aims to solve an optimization problem for a boolean formula

(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000)

(declare-const a0 Int) (assert (= a0 2))
(declare-const b0 Int) (assert (= b0 2))
(declare-const c0 Int) (assert (= c0 (- 99999)))
(declare-const d0 Int) (assert (= d0 99999))
(declare-const e0 Int) (assert (= e0 49))
(declare-const f0 Int) (assert (= f0 49))

(declare-const a1 Int) (assert (= a1 3))
(declare-const b1 Int) (assert (= b1 3))
(declare-const c1 Int) (assert (= c1 (- 99999)))
(declare-const d1 Int) (assert (= d1 99999))
(declare-const e1 Int) (assert (= e1 48))
(declare-const f1 Int) (assert (= f1 49))

(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)

(define-fun max ((x Int) (y Int)) Int
  (ite (>= x y) x y))

(define-fun min ((x Int) (y Int)) Int
  (ite (< x y) x y))

(define-fun goal ((c Int) (d Int) (e Int) (f Int)) Int
  (* (- d c) (- f e)))

(define-fun sat ((c Int) (d Int) (e Int) (f Int)) Bool
   (and (and  (>= d c) (>= f e))
        (forall ((x Int)) (=> (and (<= a0 x) (<= x b0))
                              (> (max c (+ x e)) (min d (+ x f)))))))

(assert (and (sat c d e f)
             (forall ((cp Int) (dp Int) (ep Int) (fp Int)) (=> (sat cp dp ep fp)
                                                               (>= (goal c d e f) (goal cp dp ep fp))))))

(check-sat)

I guess it is because of the quantifiers and the implication, this code costs a lot. When I tested it on line, it gave me 2 warnings, and the final result is unknown:

failed to find a pattern for quantifier (quantifier id: k!33)
using non nested arith. pattern (quantifier id: k!48), the weight was increased to 1000000000 (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>). timeout`. 

Could anyone tell me if it is these 2 warnings which avoid from getting a good result? Is there any way to optimize this piece of code so that it runs?

回答1:

I have solved optimization problems in Z3 in the following, iterative way, essentially a loop that searches for a solution by using several invocations of Z3.

1. Find one solution (in your case, a solution to (sat c d e f)

2. Compute the value of that solution (if your solution is c0, d0, e0, f0, evaluate (goal c0 d0 e0 f0). Call that value v0.

3. Find a solution to the new problem (and (sat c1 d1 e1 f1) (> (goal c1 d1 e1 f1) v0)).

4. If point 3. returns UNSAT, v0 is your maximum. If not, use the new solution as v0 and go back to point 3.

You can sometimes speed up the process by guessing an upper bound first (i.e. values cu, du, eu, fu such that (and (sat c d e f) (<= (goal cu du eu fu)) is UNSAT) and then proceeding by dichotomy.

In my experience, the iterative way is much faster than using quantifiers for optimization problems.

回答2:

SoftTimur: Since your problem involves non-linear arithmetic (in the goal function) over integers, Z3 is likely to respond "unknown" to your problem even if you can solve other issues that you've come across. Non-linear integer arithmetic is undecidable, and it's unlikely that the current solver in Z3 can efficiently handle your problem in the presence of quantifiers. (Of course, the amazing Z3 folks can tweak their solver just "right" to address this particular problem, but the undecidability issue remains in general.) Even if you didn't have any non-linear constructs, quantifiers are a soft spot for SMT solvers, and you're unlikely to go far with the quantified approach.

So, you're essentially left with Philippe's idea of using iteration. I want to emphasize, however, that the two methods (iteration vs quantification) are not equivalent! In theory, the quantified approach is more powerful. For instance, if you ask Z3 to give you the largest integer value (a simple maximization problem, where the cost is the value of the integer itself), it'll correctly tell you that no such integer exists. If you follow the iterative approach, however, you'll loop forever. In general, the iterative approach will fail in cases where there is no global maximum/minimum to the optimization problem. Ideally, the quantifier based approach can deal with such cases, but then it's subject to other limitations as you've observed yourself.

As great as Z3 (and SMT solvers in general) is, programming them using SMT-Lib is a bit of a pain. That's why many people are building easier to use interfaces. If you're open to using Haskell for instance, you can try the SBV bindings which will let you script Z3 from Haskell. In fact, I've coded up your problem in Haskell: http://gist.github.com/1485092. (Bear in mind that I might've misunderstood your SMTLib code, or maybe made a coding mistake, so please double check.)

Haskell's SBV library allows both quantified and iterative approaches to optimization. When I try z3 with quantifiers, Z3 indeed returns "unknown", meaning the problem is not decidable. (See the function "test1" in the program.) When I tried to iterative version (see the function "test2"), it keeps finding better and better solutions, I killed it after about 10 minutes with the following solution found:

*** Round 3128 ****************************
*** Solution: [4,42399,-1,0]
*** Value   : 42395 :: SInteger

Do you happen to know whether this particular instance of your problem actually has an optimal solution? If that's the case, you can let the program run for longer and it'll eventually find it, otherwise it'll go forever.

Let me know if you choose to explore the Haskell path and if you have any issues with it.