How to optimize a code fragment in Z3? (PI_NON_NESTED_ARITH_WEIGHT)

Question

I have code in z3 whose purpose is to solve the 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 (>= xy) xy)) (define-fun min ((x Int) (y Int)) Int (ite (< xy) xy)) (define-fun goal ((c Int) (d Int) (e Int) (f Int)) Int (* (- dc) (- fe))) (define-fun sat ((c Int) (d Int) (e Int) (f Int)) Bool (and (and (>= dc) (>= fe)) (forall ((x Int)) (=> (and (<= a0 x) (<= x b0)) (> (max c (+ xe)) (min d (+ xf))))))) (assert (and (sat cdef) (forall ((cp Int) (dp Int) (ep Int) (fp Int)) (=> (sat cp dp ep fp) (>= (goal cdef) (goal cp dp ep fp)))))) (check-sat) 

I think that because of quantifiers and implication, this code costs a lot. When I tested it online, it gave me 2 warnings, and the end 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`. 

Can someone tell me if these are two warnings that do not allow to get a good result? Is there a way to optimize this piece of code so that it works?

Answer 1

I solved the optimization problems in Z3 as follows, in an iterative way, essentially a loop that is looking for a solution using multiple Z3 calls.

• Find one solution (in your case - solution (sat cdef)

• Calculate the value of this solution (if your solution is c0 , d0 , e0 , f0 , evaluate (goal c0 d0 e0 f0) . Call this value v0 .

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

• If point 3. returns UNSAT, v0 is your maximum. If not, use a new solution like v0 and go back to step 3.

Sometimes you can speed up the process by guessing the upper bound first (i.e. values cu , du , eu , fu such that (and (sat cdef) (<= (goal cu du eu fu)) is UNSAT) and then continue using a dichotomy.

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

Answer 2

SoftTimur: since your problem is related to non-linear arithmetic (in the objective function) over integers, Z3 will most likely answer “unknown” to your problem, even if you can solve other problems that you have encountered. Non-linear integer arithmetic is unsolvable, and it is unlikely that the current solver in Z3 can effectively handle your problem with quantifiers. (Of course, amazing Z3 people can only fine-tune their solver to solve this particular problem, but the unsolvability problem remains the whole.) Even if you didn't have any nonlinear constructions, quantifiers are a soft spot for SMT and you are unlikely to go far with a quantitative approach.

So, you essentially abandoned Philip’s idea of ​​using iteration. I want to emphasize, however, that the two methods (iteration versus quantification) are not equivalent! Theoretically, the quantitative approach is more powerful. For example, if you ask Z3 to give you the largest integer value (a simple maximization problem where cost is the value of the whole itself), it will correctly tell you that such an integer does not exist. However, if you follow an iterative approach, you will go in cycles forever. In the general case, an iterative approach will fail if the global maximum / minimum is not set for optimization. Ideally, a quantifier-based approach can deal with such cases, but then it obeys other constraints that you yourself have observed.

Like Z3 (and SMT solvers in general), programming them with SMT-Lib is a bit painful. This is why many people create easier-to-use interfaces. If you are open to using Haskell, for example, you can try SBV bindings that will allow you to script Z3 from Haskell. In fact, I encoded your problem in Haskell: http://gist.github.com/1485092 . (Keep in mind that I may have misunderstood your SMTLib code or may have made a coding error, so please double check.)

The Haskell SBV library allows you to optimize both quantitative and iterative approaches to optimization. When I try z3 with quantifiers, Z3 really returns "unknown", which means the problem is not solvable. (See the "test1" function in the program.) When I tried to execute the iterative version (see the "test2" function), it continues to find the best and best 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 know if this particular instance of your problem really has the optimal solution? If this happens, you can let the program work longer, and in the end it will find it, otherwise it will be forever.

Let me know if you decide to explore the Haskell path, and if you have any problems with it.