Why a problem with optimization goal can be faster than the case without optimization?

[dlzrmr99]

I created a project with z3 which aims to find the solution to a scheduling problem. The problem is based on 5G communication resource scheduling serving several traffic flows. The optimization goal is to find a schedule that can maximize the number of supported traffic flows. For the case without optimization, all the constraints are the same. The only difference is that 'without optimization' requires that all traffic flows should be supported. After that, I test the running time of these two cases. They have the same inputs. Also, for the 'with optimization', I select the sample that can support all traffic flow. Hence, for all selected samples, the inputs and the final supported traffic flows are the same while the scheduling information varies. However, when I compared the solving time, I find that in some cases (almost half) 'without optimization' has a higher solving time compared to 'with optimization'. It's so weird and counter-intuitive. I also checked the schedule outputs, they are all correct. I realized that it may be due to the different optimization paths even though 'with optimization' and 'without optimization' got a very close result. It would be very appreciated for you to help to explain this weird thing.

[NikolajBjorner]

The optimization engine uses different pre-processing than the solver engine.
It also may dispatch a different backend for solving arithmetical formulas (smt.arith.solver=2 vs. smt.arith.solver=6 option).
These factors could make a difference.

Other than that, you have to dig deeper.