Performance regression from arith.solver=2 to arith.solver=6

[rixed]

Hello!

I've noticed a very significant slow down past z3 v4.8.10, that I've bisected to originates without any doubt from the above mentioned commit. I have very long smt2 files that uses only a few short bitvectors, that suddenly went from processing for 5 seconds to 5 minutes.

I haven't managed to produce a small reproductible sample, but I attach a 500k smt2 file that demonstrate the problem (somewhat simplified from the original, takes only 50s of processing vs 5s, still very noticeable slow down). small.smt2.zip

[NikolajBjorner]

b1606487f08cec8d950be078ac31881fc36a7bea

[NikolajBjorner]

This is a place where z3 falls back to a generic optimization loop:

(define-fun cost-of-number ((t Type)) Int
(ite ((_ is int) t)
(bv2nat (int-bytes t))
(ite (= float t) 14 0)))
(minimize (+ 0 (cost-of-number t6) (cost-of-number t3327) (cost-of-number t3324) (cost-of-number t3321) (cost-of-number t3318) (cost-of-number t3315) (cost-of-number t3312) (cost-of-number t3309) (cost-of-number t3306) (cost-of-number t3303) (cost-of-number t3300) (cost-of-number t3297) (cost-of-number t3294) (cost-of-number t3291) (cost-of-number t3288) (cost-of-number t3285) (cost-of-number t3282) (cost-of-number t3279) (cost-of-number t3276) (cost-of-number t3273) (cost-of-number t3270) (cost-of-number t3267) (cost-of-number t3264) (cost-of-number t3261) (cost-of-number t3258) (cost-of-number t3255) (cost-of-number t3252) (cost-of-number t3249) (cost-of-number t3246) (cost-of-number t3243) (cost-of-number t3240) (cost-of-number t3237) (cost-of-number t3234) (cost-of-number t3231) (cost-of-number t3228) (cost-of-number t1248) (cost-of-number t1249) (cost-of-number t1250) (cost-of-number t1252) (cost-of-number t1287) (cost-of-number t1288) (cost-of-number t1292) (cost-of-number t1293) (cost-of-number t1299) (cost-of-number t1305) (cost-of-number t1306) (cost-of-number t1307) (cost-of-number t1309) (cost-of-number t1344) (cost-of-number t1345) (cost-of-number t1349) (cost-of-number t1350) (cost-of-number t1356) (cost-of-number t1363) (cost-of-number t1364) (cost-of-number t1371) (cost-of-number t1372) (cost-of-number t1379) (cost-of-number t1380) (cost-of-number t1390) (cost-of-number t5) (cost-of-number t4380) (cost-of-number t4377) (cost-of-number t4374) (cost-of-number t4371) (cost-of-number t4368) (cost-of-number t4365) (cost-of-number t4362) (cost-of-number t4359) (cost-of-number t4356) (cost-of-number t4353) 

Seems it would be possible to tease out a weighted max-sat version of this (assert-soft ...) instead of minimize with weighted constraints. You use 4 bit numbers so every variable, t6, etc. maybe has 17 soft constraints based on dispatch.

[rixed]

Note: setting smt.arith.solver to 2 (as suggested by other perf related issues) significantly improve performances (for all z3 versions mentioned above, but especially post 4.8.10)

[NikolajBjorner]

Consider encodings of this form:

(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv1 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv2 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv3 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv4 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv5 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv6 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv7 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv8 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv9 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv10 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv11 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv12 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv13 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv14 4))) :weight 1)
(assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv15 4))) :weight 1)
(assert-soft (not (= float t6)) :weight 14)

(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv1 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv2 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv3 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv4 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv5 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv6 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv7 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv8 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv9 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv10 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv11 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv12 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv13 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv14 4))) :weight 1)
(assert-soft (=> ((_ is int) t3327) (bvult (int-bytes t3327) (_ bv15 4))) :weight 1)
(assert-soft (not (= float t3327)) :weight 14)

Then z3 uses the maxsat engine instead of the weaker primal simplex and MIP for optimization.

[NikolajBjorner]

The performance regression introduced by b1606487f08cec8d950be078ac31881fc36a7bea was fixed earlier this week. It is orthogonal to the difference between arith.solver=2 and arith.solver=6. There is indeed a noticeable difference.

[NikolajBjorner]

I am relabeling the bug because it is the same example.

[NikolajBjorner]

So far the perf difference is centered around equality propagation. Tuning for this benchmark doesn't seem to help other benchmarks that I tried so far. It might even hurt very slightly, but this is within the margin on fluctuation. The current status is that the new solver is at most 2x slower on this benchmark. I would appreciate if you could let me know if you can or can't replicate my findings on other benchmarks with the latest push.

[rixed]

Thank you very much for following up. I'll try master sometime next week.

[rixed]

Comparing head to head z3 v4.8.10 versus HEAD (b6f7deacf4d) v4.8.10 is still several times faster than HEAD. z3 v4.8.12 perform roughly the same as HEAD.

Actual numbers show that my benchmark is about 3 times faster on v4.8.10, and the benchmark include many other things than just processing with z3, so the actual speed difference for z3 alone is likely significantly larger than that.

I haven't implemented yet your suggestion to use soft assertions. It is my intention to give this a try but I have no time to schedule this in the foreseeable future, so for now I'll just stick to the latest z3 that works for me.